Hacker News new | past | comments | ask | show | jobs | submit login

It's the exact opposite of "you cannot make language X safer", only if you define that as "given enough time and resources, you could make a proof that your program is correct".

But that's not a safe language; that's a safe work. ANY programming work - regardless of language - can be made safe via such expensive means, which puts this square into the space of "argument ad absurdum". You could argue that brainfuck or assembler can be made safe via these means, but everyone would rightly ridicule you for it.




Maybe I'm crazy but "being a god" is much higher bar than "given enough time and resources, you could make a proof that your program is correct". Moreover, unlike your bf analogy: Sel4 exists, and is in use, and is used in safety-critical applications such as military drones.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: