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

Contrary to common belief, it is possible and easy to prove programs correct <em>if only proper programming languages are used</em>.

This makes it possible to check software, to not launch a $10 billion rocket before you're sure the software is perfect, and to trust software that comes with 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 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.

<ul class="links">
<li>_(Formal methods| http://www.comlab.ox.ac.uk/archive/formal-methods.html) for correct programming.
<li>_(Semantics-Based Program Analysis and Manipulation| http://www.cs.cmu.edu/afs/cs.cmu.edu/user/wls/www/sbpm.html).
</ul>
