5 Jan
2012
5 Jan
'12
6:33 p.m.
Dijkstra was
more interested in whether you could prove that your
program behaved according to its specification.
The problem is that it doesn't
account for buggy specifications; once
you can prove that your program adheres to the specification, you
just need to prove that your specification is written correctly. In
other words, we're now debugging our specifications instead of our
programs and the problem hasn't substantially changed. The specifications will always need to be written in
something that
can be digested by a computer in order to prove the program correct,
...the prover will make mistakes (due to bugs, if automated; no piece
of software the size of a program prover is without bugs).
so now I've just shifted the problem of writing a
correct program to
writing a correct specification.
And added the problem of constructing code that provably implements
that specification. (This might be automatable, in which case it's
just a compiler for a new language.)
"Beware of bugs in the above code. I have only proved it correct, not
actually tried it." (From memory, probably not quite exact.)
/~\ The ASCII Mouse
\ / Ribbon Campaign
X Against HTML mouse at rodents-montreal.org
/ \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B