| ▲ | Animats 4 hours ago | |
> "there is just no perfect correctness possible in the Turing machine model" Grrr. Clueless people keep saying that. People have been verifying programs for over forty years now. Formal correctness in terms of not violating assertions is possible for most useful programs. As someone pointed out about the Microsoft Static Driver Verifier, if you're program is anywhere near undecidability, it has no business being in the kernel. This not a legit criticism. | ||
| ▲ | PaulHoule 3 hours ago | parent | next [-] | |
Theorem prover ideas have an impact on Java, Rust and a lot of languages —- it really would be great to see something that accomplishes even more…. Would be nice if you could have a program that lives side by side with a correctness proof. | ||
| ▲ | PaulDavisThe1st 29 minutes ago | parent | prev [-] | |
> if you're program is anywhere near undecidability, it has no business being in the kernel. who the hell cares just about "the kernel" (whatever kernel that is) ? I write native desktop applications and they are completely unverifiable. | ||