On Wed, Jun 22, 2011 at 8:11 AM, Dominic Mulligan < dominic.p.mulli...@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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe