After reading this article I got excited. Apparently it is possible to create a proof language that is both performant, total and reliable. This is one of the things that drew me to Haskell - the idea that the language and compiler should be able to enforce strict rules of correctness. It does not support dependent types though and therefore cannot prove most theorems. Dependent types allows for value level computations at compile time and makes it possible to constrain types arbitrarily. This is because there is no native types and types are at the same level as values and can be used as values.