Formal methods, automated theorem provers and safer languages have come some ways since I started in the era of staring at glowing CRTs and fiddling with keys. To me, if we can't prove we're building things on a solid foundation, we're just doing one order-of-magnitude removed from writing code without tests.
0) Prove the compiler is correct.
1) Prove the OS is correct. (seL4, for example)
2) Prove programs are correct.
I think we're rapidly approaching barriers in effort, error-detection, and cognitive abilities that even the best handful of highly-skilled homo sapiens sapiens have difficulty proving/doing/scaling. At what point (or tapering era) do we more seriously consider systems for autonomously generating code# with automated correctness, worst-case and timing analysis? We have massive, massive code-bases of Linux, LLVM, OpenBSD, etc. without formal proofs but with unknown-unknown numbers of bugs... just the other day, someone working in Rust ran into an LLVM bug involving bounds checking. (Yikes!)
# Let's first make it easy by constraining the solution-space to simplistic, imperative, SSA w/ liveness (lifetimes) logic.
Formal methods, automated theorem provers and safer languages have come some ways since I started in the era of staring at glowing CRTs and fiddling with keys. To me, if we can't prove we're building things on a solid foundation, we're just doing one order-of-magnitude removed from writing code without tests.
0) Prove the compiler is correct.
1) Prove the OS is correct. (seL4, for example)
2) Prove programs are correct.
I think we're rapidly approaching barriers in effort, error-detection, and cognitive abilities that even the best handful of highly-skilled homo sapiens sapiens have difficulty proving/doing/scaling. At what point (or tapering era) do we more seriously consider systems for autonomously generating code# with automated correctness, worst-case and timing analysis? We have massive, massive code-bases of Linux, LLVM, OpenBSD, etc. without formal proofs but with unknown-unknown numbers of bugs... just the other day, someone working in Rust ran into an LLVM bug involving bounds checking. (Yikes!)
# Let's first make it easy by constraining the solution-space to simplistic, imperative, SSA w/ liveness (lifetimes) logic.