Wow! A rave from the grave.

First off, thank you for the links. I've only browsed most of then so far, but they will make for interesting reading over time.

If I am not wrong, FP-people say that absence of side effects simplify proofs of correctness (wrt specifications), not that proofs of programs with side effects are impossible.

Maybe they do, but not in most papers I've read. When I read a formal proofs paper that deals with a real world problem rather than isolated, mathematically pure problems--like incrementing a number or multiplying two numbers together--then I (and other programmers), might to start to sit up and take notes.

What do I mean by a real world problem? Let's start with something really trivial. Command line filter programs. Say wc and tee. Show me (and explain) a formal proof for one of these programs. How it will handle taking input from a local disk file; or a remote disk file; or via pipe from another program; or from the keyboard; and ditto for the sink; and still do its job.

But they never do that. Somehow, they manage to persuade someone, somewhere to pay them public money (it has to be public, because no one would fund this stuff privately), to write papers on how to "prove" a computer can successfully increment a number. And they come up with

Let's try it on a trivial example. Informally, the specification is to increase the value of integer variable x . Formally, we face a problem: we are given no way to relate the final value of a variable to its initial value. We have to use a trick: introduce an extra variable, not part of the state space, to carry the relation. We write

∀X� {x = X} S {x > X}

meaning: whatever x may have been equal to at the start, it is greater than that at the end. For S we might propose the assignment x:= x+1 . To prove it correct, we must use the assignment rule {substitute e for x in R } x:= e {R} In the example, this means

{x+1 > X} x:= x+1 {x > X}

The precondition is not what we want, so we now use the consequence rule (∀σ� A ⇒ P) ∧ {P} S {R} ∧ (∀σ� R ⇒ Z) ⇒ {A} S {Z} where σ (the state) stands for all variables. In the example, this means we must prove

∀x� (x = X) ⇒ (x+1 > X)

which is now a simple theorem of ordinary logic. All that, just to prove the obvious!

No shit Sherlock. All of that, to prove $i++? And that doesn't even handle the case where $i = 2147483648;. They'll undoubtedly determine that the outcome of incrementing that to be 2147483649, but the reality is, on 32-bit computers systems that it might be. Or it might be -1.

But that formalism above won't consider the case of what happens when you increment a signed integer across its register size boundaries, because mathematicians live in a theoretical world of Real and Natural (who knows how many other obscure theoretically infinite, mathematically convenient) number domains, and none of them pay the slightest consideration to mundane realities like register sizes and word lengths.

Now lets look at what they come up with for multiplying two numbers. This is the modern, advanced, abbreviated, compacted version. See the last linked paper above, page 9 for the unabridged nightmare:

x' = x y�: s:= 0; s' = s + x y; x:= s

s' = s + x y�: if y=0 then ok

else if even(y) then (x:= x 2; y:= y/2; s' = s + x y)

else (s:= s+x; x:= x 2; y:= (y–1)/2; s' = s + x y)

I won't pretend to fully understand that, so I'll ask a few questions: Does it handle register overflow? How about one or both inputs being #NaN? Or either or both being one of the two flavours of infinity?

I'm not mathematician, but take a closer look at the case above where if y=0 then ok. According to the paper, "ok is the identity relation and then later on "The empty (do nothing) program ok is the identity relation". Que? The way I read that, if the second (or one of?), the inputs to multiplying two numbers is zero, we do nothing! So-orry, but my schoolboy arithmetic tells me that anything times zero is zero--not throw your arms up in disgust and do nothing.

Bad rhetoric

I realise that the author is a much clever person than I am, but right from the start of this paper there are a bunch of things that just don't ring true.

Formal programming methods allows us to prove that a computation does what its specification says it should do. More importantly, formal methods help us to write specifications, and to design programs so that their computations will provably satisfy a specification.

This is analogous to the use of mathematics in all professional engineering: civil engineers must know and apply the theories of geometry and material stress; electrical engineers must know and apply electromagnetic theory.

So why don't software engineers know and apply a theory of programming?

I've broken that into three paragraphs. The first is the sales pitch. A broad-termed, theoretically desirable goal. A panacea. A magic bullet.

The second paragraph is supporting argument.

• Argumentum ad verecundiam

  in all professional engineering

  Most civil engineers to not use theories of geometry and material stress. They use tables.

  If this member is at this angle carrying this load, it will need to be--scan across for the angle, scan down for the load--this strong. And looking that up in the manufacturers tables for (say) steel girders or reinforced concrete lintels, including the statutory increment for safe working load for this type of construction, it will need to have this cross-sectional area. And that means part number xyz. Of course, for the most part these days, they'll feed their proposed design into a finite element analysis simulation, and increase the strength of the members until they eliminate any "hot spots".

  And an electrical engineer will rarely need to remember, let alone actually calculate any "electromagnetic theory" once he's left college. It's mostly just a case of picking the appropriately rated parts from the manufacturers catalog. Sure, someone somewhere had to design those parts, but I guarantee that not one single rating was arrived at through mathematical processes. The ratings are arrived at by testing--probably to destruction--and then applying a substantial "fudge factor" to indemnify the manufacturer against failures when close to the limits.

  As an example, there is a whole sub-culture of computer geeks that get their jollies by seeing how far the can push the clock rates of cpus beyond the manufacturers ratings.

• Cum hoc ergo propter hoc.

  The paper postulates that because of the use of mathematics in all professional engineering, all programs should be written using the theories of mathematics. And all programmers should be mathematicians.

  Except, as I've shown above, the cum hoc is false, hence the ergo doesn't.

To date, in all the sources I've read, mathematicians completely miss the point about engineering.

Engineering is not about specifying products, from the ground up, in logically provable, theoretical terms. Engineering is about about assembling a collection of standard parts, to meet a set of requirements, in a timely fashion, for the lowest cost. And whilst some of those requirements will be measurable in ISO units: speed, weight, strength etc. Another bunch of requirements will be ethereal things like looks, feel, affects on the environment, impact on the view, life-time costs, built-in obsolescence, usability, desirability, etc.

And the impact of those ethereal elements on the success of products becomes ever more important. Take the success of things like:

• the mediocre technical capabilities of the iPhone:

  but boy does that interface ever make for good TV ads.

• the heavy, slow and expensive Toyota Prius:

  it's not that much more fuel efficient than a modern say 1.2 litre VVT petrol engined four seater, and far less fuel efficient than a modern, common rail 1.4 diesel engined equivalent.

  The secret of its success? You cannot mistake a Prius for anything else. And there are no 200+ HP, 16-valve, turbo charged variants of it. So when you pull up along side the red carpet in it, amongst all the 40' long, gas-guzzling stretched limos, no one is in any doubt that "you care".

  Even if you did just fly half way around the world in your private jet to attend.

Engineering is not theoretical

Engineering is not about proving that the product complies with theories. It's about satisfying a few theoretically quantifiable requirements, and a whole bunch more unquantifiable ones. Read about the construction of the Millau Viaduct. A very small part of the effort involved the solving of well-known formulae ensuring the strength of the beams, cables and towers. A larger proportion was to do with the logistics of constructing those huge skinny towers in a "continuous pour", running the cables and manoeuvring the decks into position.

But a far larger proportion of the effort was involved in minimising the impact of the construction on the environment; ensuring the aesthetics of the final construction; engendering national pride in the French psyche.

Very few if any software projects have anything like these logistics and emotional criteria to deal with.

Dark Ages

In engineering terms, the software industry is currently, roughly equivalent to the 16th century cathedral building industry in terms of sophistication. Like them, we build each construction from scratch, individually, to fit its landscape. Each building block is carved to fit its individual neighbours. We build the infrastructure just as thick as we think it needs to be, and if it starts to fall down when we're half way up, we build it thicker.

In metalworking terms, we may no longer need to start by extracting the raw metal from the ore, but we are still at the point of fettling pieces of standard stock to manufacture individual components.

Software development has as much to do with "engineering" as does cookery. Indeed, cookery is now routinely done on a mass production, engineering scale, and software hasn't even come close to achieving that.

I sit here at this computer with a dozen or more languages installed and, despite the theoretically provable, analysed and documented to death nature of a simple sort function, there are probably 2 or 3 dozen implementations of quicksort in the various libraries on my system. And they probably all have bugs.

Until we start constructing programs from standard parts, the terms 'software' and 'engineering' do not belong in the same sentence. And I don't mean standard libraries of functions, or extended class hierarchies.

The former come in huge great globs of disparate facilities all lumped together into single linkable, statically or dynamically, chunks. If I want to replace a single function, be it sort() or strcmp(), I have to replace everything else it's library contains also. And that means re-testing everything.

And the latter is source code. The approximate equivalent of blueprints. To replace the implementation of a single class means rebuilding the program (and every program) that uses it. And that means re-testing everything from scratch.

More craft than engineering

Until OSs provide us with a catalog of standard parts, specified in high-level, generic terms, that we can replace individually, and assemble together, at runtime, into higher level sub-components; test in the abstract and then assemble those into higher level components still; software development will remain more craft than engineering.

And formal methodologies will remain a theoretical pipe dream beloved of academics but largely ignored by the industry just as it has, as pointed out by the paper, ever since Hoare first proposed it in 1969.

It took metalworking nearly two millenia to move from the bronze age to engineering. I doubt that software will take quite so long, but we are currently still somewhere in the Dark Ages and (IMO) Hehner's optimism: "I am optimistic that Kieburtz is right, that the use of formal design methods is just around the corner." is still wildly misplaced.