Posts
Formal software correctness is gaining traction, with a paroxysmal application to lethal issues in medicine and autonomous vehicles. Interactive proof assistants based on type theory have shown their effectiveness to prove the correctness of important pieces of software like a C compiler [Ler09] or a software-to-hardware toolchain [DeepSpec]. However, they suffer from a major limitation: the absence of effects.
Effects and proof assistants: An impossible marriage? The general acceptance of interactive proof assistants by non-experts suffers from a major limitation, the absence of effects in their type theory. Indeed, some basic programming paradigms – such as exceptions or mutable memory – are absent from the language of type theory, leading to efficiency issues. Dually, some basic logical principles – such as the excluded middle or the axiom of choice – are also absent from the language, leading to expressivity issues. Taking aside the lack of efficiency and expressivity, the absence of effects forces developers to stay in the “all programs and proofs must be fully specified and terminating” paradigm, which prevents quick prototyping and testing before entering the full certification process...
A more conceptual cause of the incompatibility between effects and type theory lies in what is known as the Curry-Howard correspondence, which tells us that proofs and programs are the very same things. Therefore, extending the expressivity of the language from a programming point of view amounts to extending the expressivity of the logic, which can lead to inconsistencies if the extension is not compatible with the rest of the logical system.
Read more...
Source: Open Access Government
