[Haskell-cafe] formal methods & functional programming

[Lennart Augustsson]

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