comp.lang.ada
 help / color / mirror / Atom feed
From: "amado.alves" <amado.alves@netcabo.pt>
To: <comp.lang.ada@ada-france.org>
Subject: RE: Software Design
Date: Sat, 13 Dec 2003 02:18:27 -0000
Date: 2003-12-13T02:18:27+00:00	[thread overview]
Message-ID: <mailman.109.1071281924.31149.comp.lang.ada@ada-france.org> (raw)

<<
> "There are two ways of constructing a software design. One way is to
> make it so simple that there are obviously no deficiencies. And the
> other way is to make it so complicated that there are no obvious
>deficiencies." C. A. R. Hoare

It will be very interesting to see an operating system or at least
a (visual) text editor, which has obviously no deficiencies, and
at the same time is useful.

I'd like to propose new term "hoareware" for the kind of software
for which the quoted phrase is true.
>>

Cool name. But what's the denotation? I take it you mean (just) the second sentence in Hoare's paragraph. The "correctness by construction" series of papers by Peter Amey touch this (Google for it). Personally I want to believe. 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. So in sum I think I agree with what I think you're conjecturing: that for a piece of software to be useful it must be complex by necessity. But the lesson from mathematics says a complex thing can be shown correct. 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."
 
(Sorry if I sound rambling. I am :-)
 
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."
 



             reply	other threads:[~2003-12-13  2:18 UTC|newest]

Thread overview: 8+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2003-12-13  2:18 amado.alves [this message]
2003-12-13 13:40 ` Software Design (see below)
2003-12-15 12:41   ` Peter Amey
     [not found] <468D78E4EE5C6A4093A4C00F29DF513D04B82AFF@VS2.hdi.tvcabo>
2003-12-13 21:22 ` Alexandre E. Kopilovitch
  -- strict thread matches above, loose matches on Subject: below --
2003-12-12 14:43 Robert Spooner
2003-12-12 15:22 ` Peter Hermann
2003-12-12 15:55 ` (see below)
2003-12-12 19:49 ` Alexandre E. Kopilovitch
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox