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

Rafael C. de Almeida almeidaraf at gmail.com
Mon Sep 15 12:05:11 EDT 2008


Richard A. O'Keefe wrote:
> 
> 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".

I do not know. I'm not experienced on the field and I was under the
impression you'd write your code then get a pen and a paper and try to
prove some property of it.

Someone mentioned coq, I read a bit about it, but it looked really
foreign to me. The idea is to somehow prove somethings based only on the
specification and, after that, you write your code, based on your proof?
If so, what's the difference of that and writing the same program twice
in two different languages? Isn't that kind of what's going on anyways?

> 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!"

Do they operate with Haskell functions directly? I mean, can I somehow
import the functions I wrote in Haskell and try to prove properties on
it using those tools you talk about?

>> 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.
> 

Hm. I've used quickcheck, I find it really nice. It was definetely the
tool I had in mind when I was arguing about tests being enough to
'proof' things. Anyhow, I'll take a look on that article, maybe it
already answers lots of the questions I've raised here :-).


More information about the Haskell-Cafe mailing list