RE: Software Design

["Alexandre E. Kopilovitch" <aek@vib.usr.pu.ru>]

amado.alves wrote:

>I dream of complex programs
>being proved correct just like complex mathematical proofs: by revision.

There is a common misconception (among non-mathematicians) about the nature
and power of mathematical proofs: those proofs do not signify for a final
and eternal truth as many non-mathematicians believe; a proof just exposes
a logic which leads to the theorem's conclusion. So anyone who relies upon
a theorem is supposed to check and agree with that logic. Because of that,
too complex proofs have less value in mathematics then simple proofs (too
few people can actually inspect the logic of, say, 100-page highly demanding
mathematical text), and therefore inventing of a new, simple and
straightforward proof for already proven (but only by lengthy and complex
proof) theorem is always regarded as quite respectable mathematical result.

> 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."

Obviuosly, the language, terminology and notation used in a proof greatly
influences reader's ability to inspect its logic. A clear language,
well-chosen and stable terminology and notation are if fact prerequisites
for wide and effective use of a mathematical result. In this sense Ada
language is certainly on right way - Ada strives to provide exactly that -
clear, well-chosen and stable notation as well as basic level of the language
for programs/software, and a good exposition of a logic and intentions is
a highly useful thing even if it is somehow incomplete and/or unpolished
regarding to mathematical standards.

But anyway, what should be never forgotten - equally in software engineering
and in mathematical applications - that both ends of a proved thing must be
checked every time: that actual prerequisites are strong enough for the proof
to be applicable and that the theorem's conclusion is enough to satisfy
actual requirements. And this is the most critical point in usage of "already
proved" things.



Alexander Kopilovitch                      aek@vib.usr.pu.ru
Saint-Petersburg
Russia