> "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.
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.
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.