Robin Green wrote:
2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example "Why Dependent Types Matter" by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple "sized types" such as "a list of length 6". For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly "natural" style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs).
I would just like to point out that there is nothing that forces you to "thread" the proofs through the programs. With dependent types you have this option, but you can also write standard "Haskell" code and have your proofs be separate. It's up to you to choose which way you do things. (If you do separate proofs you can even add some construct to the logic that makes it classical if you like.) Furthermore, I don't see such a clear separation between your points 1 and 2. With dependent types you are making proofs and then using them as programs. How much extraction you do is a matter of optimization, I'd say. And how efficient the extracted program is depends on which proof you choose to do. -- Lennart