[Haskell-cafe] Verifying Haskell programs vs. generating verified Haskell programs

[Alexander Solla]

On Wed, Jun 22, 2011 at 8:11 AM, Dominic Mulligan <
dominic.p.mulligan at googlemail.com> wrote:


> > There's a second (haha) approach, which I use basically every day.
>
> > Use the typing language fragment from a strongly typed programming
> language to express a specification, and then rely on "free"
> functions/theorems and the Howard-Curry isomorphism theorem to guarantee
> correctness of implementation relative to the specification.
>
> How does this count as a distinct approach to the problem?  It's
> essentially what happens when you verify a program in Coq.
>
> Further, there's much too sharp a distinction in the OP's mind between
> constructing a verified program in a proof assistant and verifying an
> existing program.


Yes, I agree about your further point.  And if we agree there is
little-to-no distinction between using an external tool and an internal
sub-language, my point becomes even weaker.

But I do think we can agree there is some difference between a total
language (i.e., a proof assistant) versus a partial language with strong
typing (like Haskell) versus a memory-poking-and-peeking magma (like C).

My point was that we don't necessarily have to go for a total language to
get logical proof.  We can instead rely on derivable/free functions for most
of the verification, and paper-and-pencil proof/proof by inspection/etc. for
the rest.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110622/777eb952/attachment.htm>