I was fully prepared to hate this article, given the long list of previous “I have no clue how formal proof tools work, yet have strong opinions about how useless they are” articles.
Instead, I was pleasantly surprised by how balanced it was.
What convinced me that formally proving software correct is possible were seL4, CompCert, and my own experience proving small projects correct using Lean and Rocq.
seL4: The US military and NSA tried to break seL4. They failed.
CompCert: Researchers tested CompCert against five leading commercial and open-source C compilers. Every compiler except CompCert had bugs. Not just a few, but hundreds. CompCert had zero.
And there are now many more commercial examples of software being formally proven correct.
Maybe in the future the difference between being a programmer and being a Software Engineer will be that the software you write is proven correct.
Instead, I was pleasantly surprised by how balanced it was.
What convinced me that formally proving software correct is possible were seL4, CompCert, and my own experience proving small projects correct using Lean and Rocq.
seL4: The US military and NSA tried to break seL4. They failed.
CompCert: Researchers tested CompCert against five leading commercial and open-source C compilers. Every compiler except CompCert had bugs. Not just a few, but hundreds. CompCert had zero.
And there are now many more commercial examples of software being formally proven correct.
Maybe in the future the difference between being a programmer and being a Software Engineer will be that the software you write is proven correct.
That might actually happen with the help of AI.