[Haskell-cafe] formal methods & functional programming

[Robin Green]

Lennart Augustsson wrote:
> 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.

But wouldn't that alternate way break the principle, recommended by 
Cardelli, that all code should be well-typed and the types of all terms 
should be, shall we say, "plainly" deducible from the code alone (i.e. 
not requiring any "difficult" reasoning on the part of the human 
reader)? If not, could you give an example to illustrate your point?

>  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.

Well I thought someone might say something like that - which is why I 
called them "angles" on the question. :)

But while statements about types and statements about values might be 
inter-convertable, I think they look different and one can be more 
convenient than the other for various purposes. I've only used dependent 
types trivially so I could be wrong.

-- 
Robin