[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

[Richard A. O'Keefe]

On 14 Sep 2008, at 10:59 pm, Rafael Almeida wrote:
> One thing have always bugged me: how do you prove that you have
> correctly proven something?

This really misses the point of trying to formally verify something.
That point is that you almost certainly have NOT.  By the time you
get a theorem prover to accept your specification, you have
(a) gone through a couple of rounds of redesign (before writing the
     code!) and now have something really clear (because the prover
     is too dumb to understand subtle stuff)
(b) just done a lot of "testing" on the design that was finally
     accepted.

> I mean, when I write a code I'm formaly
> stating what I want to happen and bugs happen. If I try to prove some
> part of the code I write more formal text (which generally isn't even
> checked by a compiler);

I'm sorry?
What kind of half-arsed "formal" specification is NOT "checked"?
None of the specification tools I've played with (I really wish there
were a PVS course I could attend in NZ) can truthfully be described as
"not checked".

Symbolic model checking tools effectivley _are_ testing tools; what you
normally get from them is not a cheery "that's fine boss" but a snarky
"you forgot about this possible input didn't you, idiot!"

> how can I be sure that my proof doesn't
> contain bugs?

You can't.  What you CAN be sure of is that your previous proof
attempts DID contain bugs.  Lots of them.  At least *those* ones
are gone.  Let's face it, you can't be *sure* that you aren't a brain
in a jar being systematically deceived by a demon.  (Read Descartes.)

In fact, you can usually be CERTAIN that you haven't proved the
validity of your whole system, because you usually haven't tried.
Formal methods are a risk reduction tool.  You pick some part of the
system which has a special need for reliability, isolate it, model it,
check the model for consistency, specify operations on it, prove
something about them, and you learn a heck of a lot by doing so.
What you can't eliminate is the possibility that something nasty is
lurking in the BIOS of your computer specifically watching out for
your code so it can sabotage it.  Several times in my programming
career I have encountered perfectly correct code that malfunctioned
because of a broken compiler (well ok, in one case it was a broken
assembler).

> Why would it make my program less error-prone? Is there
> any article that tries to compare heavy testing with FM?

Lots of them.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.2475
might make a good start.
The idea that the FORTEST researchers share is that formal
methods can *help* testing.
Indeed, QuickCheck basically _is_ an 'automatic tests from
specifications' tool, one of many that have been built over the
years.

If you stop thinking of formal methods as "verifying finished
written programs" and more as some mix of "design for
checkability" (so that bugs are less likely to be written into
the code in the first place) or as "testing for specifications"
it may make more sense to you.