Proof

A term for the process of checking that a belief holds in some context.

Contrary to common belief, it is possible and would be relatively easy to prove programs correct if only proper programming languages are used.

This makes it possible to check software, to not launch a $10 billion rocket before you're sure the software is perfect, and to only trust software that comes with satisfying proofs.

Anything that can be formally specified about a program (like the fact that the program will terminate or not, or that such variable will not overflow) could be provable for a program designed with this proof in mind.

Of course, proofs do not remove the need for human checking. Firstly, proving the compliance of a program with respect to a formal specification does not make the formal specification adequate for the intended informal purpose.

Also of course, proving being an undecidable task in the general case, or at least an arbitrarily hard semi-decidable task, there will always be the need for humans to invent new methods for finding proofs, even though machines might do more and more of the task automatically.

Existing proof systems make it very difficult to have programs that are both proven correct and efficiently implemented. This is because provability and efficiency are opposite requirements for program representation, and existing systems can only manage a one representation for an object, not being able to consistently manage several of them. Hence the need for the choice of a compromise representation.

Tunes will remove the need of such compromise, by empowering the programmer with the ability to consistently manage multiple representations for a same abstract program, having at the same time a provable representation, efficiently implemented optimized versions, and the insurance that all these versions all strictly have the same behavior as for proven properties.

Some people who think they are clever will raise the above theoretical points about proof-finding not being possible in general. Of course proof-finding is not possible in general. Indeed, most programs are wrong and no amount of trying, manual or automated, could ever prove them right. But the purpose of proofs has never been and never will be to prove a random property for a general program taken at random out of the blue. On the contrary, the programs that are usefully proven correct are programs designed for a specific purpose, and architected in a certain way precisely because the programmer has an idea of how the program should be to fulfill said purpose correctly. In other words, for every intendedly correct program being developed, there is the informal proof of the correctness of said program (as it would be, if debugged) in the head of the programmer. And the purpose of a safe programming language for is to make it easy for the programmer to express not just the program, but also the proof of its correctness.

All fine and dandy until someone actually derives a proof. Once any proof has been derived the above falls apart. In at least once instance a proof has been derived.

This page is linked from: Coq   Correctness   Logic   Tactic