[Haskell-cafe] Verifying Haskell programs vs. generating verified Haskell programs
alex.solla at gmail.com
Wed Jun 22 20:41:56 CEST 2011
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe