::scr Proper software development processes

[Robin Houston]

On Mon, Oct 01, 2001 at 06:53:51PM +0100, simon wistow wrote:
> 
> Imperial had a fairly intresting CS degree

I'm starting to suspect that my perspective may be slightly skewed.
I studied CS in the Computing Laboratory in Oxford (as part of a
degree in "Maths & Computation"[1])

What I studied was largely theoretical. That's partly because I tended
to choose more theoretical courses, but I certainly wouldn't have had
the opportunity to learn Visual Basic or even UML there.

In the first year we learnt functional programming (using a
Haskell-derivative), with an emphasis on algebraic manipulations of
functional programs. Imperative programming was introduced using
Dijkstra's guarded command language, with lots about pre/post
conditions, provable correctness[2] and (the particular obsession of one
member of the dept) formal *derivations* of programs from their
specifications.

Much of it was fascinating, and I enjoyed it enormously. I've never
come to believe that it's useful though. I had at least two lecturers
who *honestly* believed that every program should be proved correct,
and preferably formally derived from its specifications. It's lunacy,
of course. Even writing a formal specification for (say) MS Word would
be a lifetime's unrewarding labour.

As for learning "how to Program without us getting het up with the
details of the language", I've yet to be convinced that's possible.
General principles can be explained of course, but even the most
abstracted language has its own idiosyncracies. Dijkstra's guarded
command language includes bizarre non-determinism not found in
ordinary languages, for example. In Haskell-family languages, you
need some ridiculously heavy category theory in order to understand
the workings of simple I/O.

I'm very much in favour of studying the theoretical aspects of
computer languages and programs, but I'm sceptical of the notion that
these theoretical studies affect the ordinary programmer. There is a
sort of trickle-down, of course: language designers and compiler
writers need to be acquainted with a certain amount of theory, and
programmers need to become acquainted with the facilities offered by
new languages. But it is my contention, for example, that
object-oriented programming didn't become relevant to the ordinary
programmer until the invention of C++.

Apologies for the semi-rant. Not *too* off-topic, I hope.

 .robin.

[1] I believe that they've since changed the name from "computation"
    to the more commonly-used "computer science"...

[2] prove parial correctness using a suitable invariant, and prove
    termination by finding a strictly decreasing non-negative variant. Of
    course these techniques can only be applied to individual loops.
    But a chain of reasoning could in principle be established to argue
    for the correctness of a larger program.

-- 
God! a red nugget: a fat egg under a dog.