3 ms·
So you end up stuck with languages like Ada, where the language can prove the correctness of your code (or rather, that your code follows the specification)?
by FreeFull 7y ago
So you end up stuck with languages like Ada, where the language can prove the correctness of your code (or rather, that your code follows the specification)?
- phkahler 7y agoSeems like I recently read that the Ada folks might want to borrow some concepts from Rust. To me that says both languages are working toward similar goals.
- jandrewrogers 7y agoCurrently modern C++ plus a ton of specialized tooling that covers much of the ground of Ada, just not built into the language. It is a balancing act to keep development from becoming unwieldy and the 80/20 rule applies. Code that is easy to verify also tends to be slow, and that is not a tradeoff you can make for some applications. No one is running something as complex as a database kernel through an end-to-end theorem prover. Design verification scales well (model checkers and similar), implementation not so much due to practical limits on what you can prove and accumulated complexity/bugs in the specification, and verification of code generation is very limited (I use the LLVM stack). Nonetheless, this gets you to a very low defect rate and it isn't like this code is being written from scratch every time. Even with a fully verified toolchain there will still be bugs. I once had a customer find a rare bug in a database engine that was ultimately caused by slight differences in behavior between microarchitectures running the same binary.