Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

The thing is that math isn't all that rigorous either. Formal methods (i.e. computer-verified proofs) are still very much the exception. Proofs are written for other humans to consume, and details tend to be glossed over. Usually this is fine, because the readers are mathematicians themselves and can fill in the gaps, but occasionally this leads to a crucial counterexample being overlooked.

Now what does make mathematics slightly more rigorous than other disciplines is the fact that once someone bothers to actually work through the details and finds a counterexample, they can convincingly demonstrate to other mathematicians that the proof is incorrect. Often, the detail in question isn't even all that important, and a workaround can be found that saves the overall proof. But software development is also rigorous in this sense; once you find a case the program handles incorrectly, you can write a testcase to show the difference between expected and actual behavior. And that doesn't usually show the whole program to be misguided, you can just rewrite a small part and things work again.

You seem to want a method that can not only make definitive statements after the fact, but that can actually ensure for almost all programs and almost all desirable properties that the program fulfills the property. But this is actually much more rigorous than most mathematicians ever bother with, and for good reason.

Complete verification requires stating every obvious fact in excruciating detail, because that is the only way to be sure that it is indeed obvious and a fact; in addition to tracking the complex interactions of the whole thing. Most humans really don't want to make this kind of mental effort, if they can avoid it. Even static type annotations are too verbose for some, which has lead most modern languages to include some form of type inference. I don't think you will see widespread adoption of formal methods before proof assistants are developed that can similarly handle most of the simple but tedious tasks, so that humans can focus on the actually important bits.



I actually think dependently-typed languages like Idris are the most promising in this area right now, at least until proof assistants get a lot better.

It's also not specifically the rigor in mathematics, but the grounding in solid principles. They have axioms, they know how to prove things, and they know which proofs to trust and why for the most part. What frustrates me most is stuff like programmers haphazardly reimplementing monads over and over again instead of moving on with what they were actually working on before the language and type system got in their way.




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: