Re: Software Design

["(see below)" <byaldnif@blueyonder.co.uk>]

On 13/12/03 2:18 am, in article
mailman.109.1071281924.31149.comp.lang.ada@ada-france.org, "amado.alves"
<amado.alves@netcabo.pt> wrote:

> And I ponder this evidence from mathematics: that really very *complex* proofs
> are found flawless, i.e. absolutely correct, e.g. (the proofs of) Fermat's
> Last Theorem, the Four Coulor Theorem.

But the Wiles proof of FLT was found to be erroneous shortly after after
publication. It has since been "debugged". Its present status is a matter of
the opinion of the mathematicians who participated in that effort, as far as
I can see. The 4CT was greeted with outright scepticism when announced. I do
not know what has happened since to confer "absolutely correct" credentials.

> a piece of software to be useful it must be complex by necessity

Agreed.

> But the lesson from mathematics says a complex thing can be shown correct.

I think this is highly questionable. Moreover, it is the proofs
(metaphorically, the programs) that are complex in the examples above. The
theorems (metaphorically, the specifications) are (very!) simply stated.
Software contends with complex, ill-defined and time-varying requirements
and specifications in a way that does not arise with these famous theorems.

>  That is, what we need is not simple: it's a way to show (and experience)
>  the complex correct. In a way, anti-Hoare. You know, "0% bugs."

Absolutely, yes. But the big problem, for software, is to know what standard
of correctness to hold the program to.

> The one piece of complex software in the world that is flawless is perhaps
> TeX. But it took decades to show that. Not satisfactory. I dream of complex
> programs being proved correct just like complex mathematical proofs: by
> revision. Clearly one way to accomplish this is to write them in a rigourous
> and readable language and of course in very good style. Hence "100% Ada."

Well, people tried and failed to prove the 4CT & FLT for hundreds of years.
8-)

-- 
Bill:Findlay chez Blue:Yonder dot:co:dot:uk (":" => "")