I am a PhD student at Inria Paris. I work on programming languages and theorem provers. My ultimate goal is to fusion these two worlds into one language. It would give an easy way for programmers to formally check their codes and simplify the usage of decision procedures for mathematicians. The Curry–Howard correspondence is already a good link but only works for purely functional languages.
The Coq system is a mature theorem prover. It provides a powerful higher-order logic, a purely functional language and an extraction mechanism to compile it efficiently to OCaml. The only missing thing is an effect system to represent mutable variables, exceptions, non-termination, inputs-outputs, coroutines, continuations or concurrency.
This effect system should respect the following requirements:
- to be visible in the type: like the monads in Haskell
- to be commutative: the combination of effects (ε1 and ε2) should be the same as (ε2 and ε1)
- to be inferable: the user should not write anything more than in an imperative language (no bind or monadic lift)
- to be purifiable: many effects can be hidden, like exceptions in a catch or mutable values hiding the reference
- to be certifiable: it should be possible to add assertions and prove them even for complex properties like serializability of concurrent algorithms
- to be compilable: the extraction mechanism should be extended for effects or, better, they should be compilable to assembly languages in a certified way
More informations can be found on my PhD page. Similar projects had been done, like Ynot, which focuses more on provability of low-level programs in Hoare-logic style.