Is Software Engineering Possible?

When the textile industry arose in the 18th century, craft was the norm in manufacturing. As the industrial revolution progressed, one after another sector of the economy made the transition from craft to industry. In 1968 it was noticed that the creation of software was a craft in a world where industry was the norm. In that year a conference was convened to address that anomaly. Those present saw themselves as participants in a momentous occasion: after this conference, Software Engineering existed, which was not the case before.

In the final paragraph of my 2009 article “Software Engineering: From Craft to Industry?” [8], I ventured to disagree. From the final paragraph:

While the processing of material leaves an irreducible residue of work for humans, in the processing of information any work that is routine instantly vanishes. Extracting the routine part from an information processing task is a creative endeavour. It is called programming. In the building of a software system any time you think you have something routine to be handed over to managed cubicle-dwelling drones, [9], you are missing an opportunity for automation. In the building of a software system there is only room for creative work. It is Craft, irreducibly so.

At the time I had read John Allen’s “Whither Software Engineering?”. I found it fascinating, but dismissed it as unrealistic and I was not convinced of its urgency. This article explains why I changed my mind.

The standard model in software development is, and has always been, to follow the test-debug cycle. I call it the standard model not because of any virtues, but because of the lack of alternatives, unless it would be to prove software correct, a notion universally rejected as utterly unrealistic (but about which more later).

The problem with the standard model can be expressed by a truism that is by now so old that nobody dares any more to utter it, or even to remember it. The problem with truisms is that some of them are true. Driven by today’s dire circumstances I’ll resurrect it here:

Testing can prove the incorrectness of code,  but not its correctness.

Ever since the days of Robert Morris, Jr (he of the worm) and Clifford Stoll (he of “The Cuckoo’s Egg”) the (implicit) thinking has been: any time now the software/hardware substrate will be good enough to network everything in sight: student records, bank accounts, patient records, to mention just some of the more ransomable things. There is no need to wait. In the blind drive to network everything in sight, ever higher towers are being built without waiting for a foundation: teetering towers in a swamp.

Such was the spectre in front of John Allen’s eyes ten years ago when he wrote his remarkable paper [1], precariously published in an obscure corner of the internet. He faces the inescapable fact that the only alternative to the test-debug cycle is proof of correctness. He sketches certain advanced concepts in logic, advanced only in the sense that they are beyond the current undergraduate curriculum. According to these concepts, proofs can be constructive, constructive in the sense of also being programs in a suitable programming language. Allen mentions the programming language ML as an example.

“Whither software engineering?” [1] was presented at the 2008 Workshop on Philosophy in Engineering. My guess is that it has been read by few, if any, of those who are in a position to do anything about the parlous state of systems software. Those few have probably dismissed the paper as an extreme example of academic lack of realism: to redo operating systems as proofs in constructive type theory! Yet … I will let a recent paper [2] speak for itself:

FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ’s theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover its state correctly without losing data.

The authors use the Coq proof assistant with a new variant of Hoare logic [3, 4]. The correctness properties are stated as theorems in the Coq variant of constructive type theory. The proofs are written by the authors and are checked by Coq running as proof assistant. The extraction feature of Coq converts the Coq programs to Haskell, the functional programming language. The resulting programs replace functions in the file system to run unmodified Unix applications such as vim, emacs, git, gcc, make, and a mail server.

There is considerable variation in performance among the various alternative file systems that can be used with Unix. Among the various benchmarks FSCQ is usually the slowest, though not by more than a factor two compared to the average of the other file systems. Thus the FSCQ project shows that Allen’s vision is technically realistic.

Is the FSCQ project the harbinger of a trend that might rescue the teetering towers? The six authors of [2] represent an unusual mix of skills, covering both systems programming and constructive type theory. The project suggests that logic can play the same role in software development as is played by mathematics in the established branches of engineering. It will take a long time before anything can happen on the required scale. The depth of change necessary make one doubt whether this is possible. Allen believes it is. To convince his readers he includes a sketch of the history of engineering.

Allen starts by reviewing the history of what is now called “software engineering”. The term was coined [5] at the conference mentioned earlier that was convened under the pressure of what was perceived at the time as “the software crisis”. It had been noticed that the problems encountered in the established branches of engineering were not nearly as severe as the ones in software development. Therefore, a new discipline called “software engineering” was called into existence, by fiat. Allen’s paper helps us understand the difference between engineering and the simulacrum thus called forth.

Established engineering programs require courses in calculus, physics, and linear algebra in the early part of the curriculum. This in spite of the fact that the students cannot yet see their use. These courses are required because the proven effectiveness of their content in engineering. For example, the behaviour of an antenna can be predicted with the theory of the electro-magnetic field, and this theory can only be understood with calculus and vector analysis. If, as often happens, a prospective “software engineer” is required to take calculus, then it is not because calculus can help to make better software.

It is not clear whether any science can help. It is only recently, with papers such as Allen’s and the one on FSCQ, that some inklings have appeared as to what kind of science can be helpful. It will take time before this clarifies and then it will take time before it is lodged in the curriculum as solidly as mathematics is in the established branches of engineering. Only then will software engineering deserve the name.

“Whither software engineering?” describes how it took a long time for the established branches of engineering to become based on mathematics. The first application of calculus in engineering may have occurred as early as 1742 with the publication by Benjamin Robins of New Principles of Gunnery. This book was adopted in the École Royale du Génie, the engineering school founded in the mid-eighteenth century in Mézières in France.

A hundred years after this, the use of mathematical methods was still controversial, at least in Britain. This was apparent when the first trans-atlantic telegraph cable was laid. The mathematical analysis by the physicist William Thomson indicated that the input signal could be of moderate voltage; the resulting weak output signal could be compensated by making the detector at the receiving end extremely sensitive. The Chief Electrician of the cable company dismissed Thomson’s mathematical analysis as “a fiction of the schools” that was contrary to common sense; common sense which dictated unprecedented high input voltages commensurate with the unprecedented length of the cable. Subjected to such an onslaught the cable failed within a few weeks [6]. Although this, and publications of William Thomson, led to the dismissal of the Chief Electrician, the battle continued for the minds of electrical practitioners between “the practical men” and “the theoretical men” till the end of the 19th century.

The École Royale du Génie, was founded in 1748. This was a step, possibly the first, of placing engineering on a mathematical foundation. Almost 150 years later the transition was not yet complete: in 1893 William Preece was inaugurated as president of the (British) Institute of Electrical Engineers. From his inaugural address:

True theory does not require the abstruse language of mathematics to make it clear and to render it respectable. … all that is solid and substantial in science and usefully applied in practice, has been made clear by relegating mathematical symbols to their proper store place—the study [7]. .

In the face of continuing increasingly disastrous failures, the practical men of today do not seem to be looking for an alternative to software that has as only credential that it has been around the test-debug cycle a number of times. Allen’s paper and the FSCQ system may offer hope for an effective alternative. Do they? If not, is software engineering possible?

Acknowledgements

Thanks to Paul McJones for pointing me to the FSCQ paper and thus providing the motivation to revisit [8].

References

[1] “Whither software engineering” by John Allen. Workshop on Philosophy and Engineering. London, 2008.
[2] “Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes” by Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nikolai Zeldovich, and Daniel Ziegler. Comm. ACM, vol. 60, no. 4 (April 2017), pp 75–84.
[3] “An axiomatic basis for computer programming” by C.A.R. Hoare. Comm. ACM 12.10 (1969): 576-580.
[4] “Ten years of Hoare’s logic: A survey—Part I” by K.R. Apt. ACM Transactions on Programming Languages and Systems (TOPLAS) 3.4 (1981): 431-483.
[5] Report on a conference sponsored by the NATO Science Committee Garmisch, Germany, 7th to 11th October 1968.
[6] Oliver Heaviside: sage in solitude by Paul Nahin. IEEE Press, 1987, page 34.
[7] Journal of the Institution of Electrical Engineers, Volume 22 (1893), Address of the President, page 63.
[8] “Software Engineering: From Craft to Industry?” by M.H. van Emden, wordpress, 2009, http://tinyurl.com/n69ymao
[9] I am aware of the biologically unfortunate analogy: it should be “worker bees in cubicles”. The Oxford English Dictionary recognizes the figurative use of “drone”, but there it means a non-working member of the community. But “drones” as in “drones in cubicles” lodged itself in the contemporary idiom: on May 20, 2017 this search string registered 1430 hits on Google.