Paul Rubin <http://[EMAIL PROTECTED]> wrote:
> Steven D'Aprano <[EMAIL PROTECTED]> writes:
> > I don't know what the state of the art is, but I suspect it
> > will be a long, long time before it is as easy as running "import
> > mymodule; verify(mymodule)".
>
> Some pretty significant pieces of software have been formally verified
> to meet their formal specifications. The trouble with
> "verify(mymodule)" is that usually means something closer to "verify
> that mymodule does what I hope it does". The computer does not yet
> have a telepathy peripheral that can read your mind and figure out
> what you are hoping, and people's attempts to express formally what
> they are hoping are easily wrong just like programs are often wrong.
Yep. I'm reminded of an ambulance dispatch system (read about it a long
time ago on the Risks mailing list, so I might be off on the detail, but
the gist should be correct) which was formally proven to obey a long
list of rules, one of which was "for this kind of emergency, an
ambulance must arrive within 10 minutes" (or the like).
Problem, of course, being that in formal logic this implies "if this
kind of emergency exists and no ambulance has arrived within 10 minutes,
you have an impossibility and from an impossibility ANY theorem can be
proven". So, if real-world road conditions meant the ambulance was
about to arrive in 10 minutes and 5 seconds, it might instead be
rerouted elsewhere... not having arrived in 10 minutes, a contradiction
was in the system and it could prove anything (I think that's know as
the theorem of Pseudo-Scotus). It's hard in (classic) logic to express
"this MUST be true; if it's false, ..." -- to human beings the first
"MUST" can be interpreted as "99.9% probability" or the like, so the "if
it's false" clause is meaningful ("in the extremely unlikely, but not
impossible since nothing's truly impossible in the real world, situation
that it's false, ..."), but to Aristotle's logic, if something MUST be
true, it's obviously irrelevant whatever might follow if that something
were instead to be false.
Alex
--
http://mail.python.org/mailman/listinfo/python-list
