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