[SystemSafety] The Fosse of Babel

[Olwen Morgan]

" ...  let us go down, and there confound their language, that they may 
not understand one another's speech.^So the Lord scattered them abroad 
from thence upon the face of all the earth ..."

Genesis 11:7-8


(No, by quoting part of the Tower of Babel story I've not suddenly gone 
all god-bothering - I'm more of a Buddhist than anything else). But this 
serves to introduce an idea:


Ask around and I expect you'd find a reasonable consensus that 
mathematics is the hardest thing in the sciences and translation is the 
hardest thing in the humanities. (As an occasional translator, FR-EN and 
DE-EN, I can certainly vouch for this as regards translation.)


Now, by the standards of hard mathematics, the kind of mathematics that 
you need to do software engineering rigorously isn't particularly hard. 
On the other hand something that is done in every software process I've 
seen is translation. We start with requirements in natural language, we 
do design in another formalism, programming in another and testing using 
yet further formalisms. Much of the use of mathematics in software 
engineering is to provide a lingua-franca that allows us to reason about 
whether a description of something in one kind of formalism is actually 
consistent with its description in a different formalism.


This makes pertinent the question of WHY the software engineering 
process is one of successive translations between different formalisms. 
Are we not asking for trouble if we have to use the most difficult thing 
in the sciences to keep us afloat because we're doing the most difficult 
thing in the humanities?


I posit that, if we ever get a firm grip on software quality, it will be 
because we have developed what I call, "end-to-end" languages - call 
them EELs for short. An EEL is a language into which we translate 
natural language requirements such that thereafter, all tasks in the 
software lifecycle can be supported directly by the EEL.

That means that an EEL must support:

1.    Statements of requirements

2.    Description of designs

3.    Low-level processing

4.    Unit and integration testing

5.    System testing

6.    Proof of correctness conditions at all life cycle stages

7.    Identification of configuration items (COBOL's Identification 
Division was prescient here - three cheers for Auntie Grace)

... and generally any other task in the life cycle related to product 
quality.


An obvious thing to do is to start designing languages that include 
annotations for; proofs, testing, configuration control, etc. Proof 
annotation are well established in SPARK Ada and within the Frama C 
project. It would be no great task to include proof annotations in a 
language itself. Proof annotations could also support automatic test 
generation.


Yet, looking at current programming languages, it's quite clear that 
we're NOT EVEN TRYING to design EELs - when the state of knowledge in 
computer science is almost certainly capable of giving an EEL suitable 
semantics and making compilers for it. What software engineering needs 
more than anything else is not new research but better application of 
what we already know.


O



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20180921/ea179f99/attachment-0001.html>