natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
A certification of a computer program is a formalized guarantee – a proof – that the program has given specified properties. For instance, it could be guaranteed to compute a given output based on a given input, or to always terminate, or to not include a certain kind of security hole.
Certifications often take the form of a proof that a program, regarded as a term of some sort (under programs as proofs), has a specified type. Thus, programming languages based on highly expressive type theories? (including dependent types) are a natural place to do certified programming “natively”. Examples are Coq and Agda. In this case, the program is written at the same time as a proof of its certification. One often then wants to “extract” the executable code or “ignore” the proof part of the terms when actually running the code, for performance reasons; Coq and Agda include mechanisms designed for this.
It is also possible to write a program in some less strongly typed language and provide an “external” certification for it, rather than one built into the program itself. Computer proof assistants like Coq and Agda are also used for this, using a formal representation of some other programming language. There are also other program analysis tools which can produce automated proofs of certain aspects of a computer program, such as safety and termination (although of course a complete solution to termination-checking is impossible, being the halting problem).
So far, fully certified programming in the type-theoretic sense is largely an academic endeavor, see for instance (SpittersKrebbersvdWeegen); the tools available at present usually require too much time and effort to be worth the payoff in industry. As automation progresses, this may change.
Adam Chlipala, Certified programming with dependent types (web)
Adam Chlipala, Implementing Certified Programming Language Tools in Dependent Type Theory PhD (2007) (web)
Discussion of the need for certified programming in scientific computation is in