"The time has come," the Walrus said,
"To talk of many things:
Of shoes--and ships--and sealing-wax--
Of cabbages--and kings--
And why the sea is boiling hot--
And whether pigs have wings."
-- Lewis Carroll (Through the Looking Glass)
Back when I was a lad Jon White taught a grad course that consisted
of a stack of papers which covered emerging areas of computer
science (e.g recursion, argued as relevant by Barron), structured
programming (Dijkstra), modular programming (Liskov), etc. It turned
out to be one of the most valuable courses I ever took.
At the time we still insisted on the need for computed GOTOs.
After all, with 4 kilobytes of memory, recursion seemed way too
theoretical to ever be practical.
Eventually I worked on implementing tail recursion in GCL and lusting
after SmallTalk. Structured programming became so obviously
good that programming using GOTOs required justification. The
new style reduced "spaghetti code" to a rare event. It greatly
decreased the error rate. Strong typing (ala PASCAL) reduced the
error rate even further, despite the side-effect of making programs
much harder to write.
These "advances" took time to develop, partly because the hardware
was not up to the task but mostly because we, as programmers,
resisted the ideas as too restrictive, too expensive, and a waste of
time. Even the notation (classes, inheritance, methods, etc) was painful.
The idea of writing provable programs has been around for a while
(Hoare, Dijkstra, etc.). It used to be that they were too hard to write
and not well-founded. But the last few years have seen the development
of systems that make writing provable programs a reasonable goal.
Writing such programs imposes yet more burdens on the programmer.
Loops should be written in a decreasing direction, functions should be
pure. They should be total in their domain. All kinds of pain points for
programmers that seem like a waste of time. Who needs Category
Theory and Inductive Construction? Even the notation is painful.
Eventually, and I believe it will be quite soon given the pace of the
internet, writing a proven program will be normal and so obviously
good that our current "just-make-it-work" style will need to be justified,
like using GOTOs. Theorem-Driven Development (TDD) will be all
the rage.
In an age when a car's brakes are computer controlled, we really do
need to prove they will be applied within 1ms under all conditions.
Computer algebra, given its strong basis in mathematics, is the ideal
setting, using the latest technology, to write proven programs. There
that are worth the time. Harper's Type Theory Foundations lectures are excellent.
"The time has come"...
...to im-prove your programming...
Tim, the Walrus.