> The only reliable way to have bug-free code is to prove it. It requires solid mathematical foundations and a programming language that allows formal proofs.

> The only reliable way to have bug-free code is to prove it. It requires solid mathematical foundations and a programming language that allows formal proofs. I'm going to be the "actually" guy and say that, actually, you can formally verify some studff about programs written in traditional/mainstream languages, like C. Matter of fact, this is a pretty lively research area, with some tools like CBMC [0] and Infer [1] also getting significant adoption in the industry. [0]: https://github.com/diffblue/cbmc https://github.com/diffblue/cbmc [1]: https://fbinfer.com/ https://fbinfer.com/