Ask HN: Should Software Be Proven?
> There is a group of people in software who believe we "should prove programs correct," much as we prove theorems in mathematics are correct. The two fallacies they commit are:
> 1. We do not actually "prove" theorems!
> 2. Many important programming problems cannot be defined sharply enough so a proof can be given; rather, the program which emerges defines the problem!
I find that any errors prevented by compilers are small and sometimes partial proofs. They definitely help. Types and generics are tremendously powerful.
That being said, I find that the current landscape includes a lot of tools that seem useless (or haven't learned to use). Here I'm thinking of things like TLA+ and dependent types (both of which I haven't explored much beyond reading).
Are specifications proofs? Are tests proofs? I don't think so, but both go pretty far in giving me confidence about my software.
I find that I'm sufficiently happy with the combination of static types, generics and testing (specification based, property based, "example" based).
What about you?