On Wed, Jun 22, 2011 at 8:11 AM, Dominic Mulligan < dominic.p.mulligan@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.