Lambda the Ultimate

i) stupid mistakes that are easy to fix ii) misconceptions about the problem domain that are hard to fix

This sort of education won't address ii) which is where the real problems lie IMO. More flexible development methodologies (e.g. XP) and more flexible languages (e.g. [insert your favourite here]) will help.

Noel

Think for example about the ill defined (or undefined) IO model in many languages. It is many times hard to tell, or simply easy toignore, what remains in the buffer after reading some data, and when exactly the EOF event is raised (after reading the EOF, after reading the last character of user data etc.)

The bugs arising from these problems are easy to fix. But consider the approach to programming they often result in: You code the program, see the bugs and then do some ad-hoc fixing. Each programmer has his own style of dealing with these issues, so reading code and being sure of its quality can be problematic. What's worse, you stop playing with the code when it seems to work. So you get used to starting with code you are unsure of, playing with the code - perhaps breaking some hidden assumptions - and stopping when you get tired or don't find any obvious bugs.

This is fine in many cases, and I have nothing against this approach to programming. But this is not the way to build provably relaible software. And more testing, yeras of SE experience shows, doesn't help much either.

I'm aware of the basic referential transparency example, but want more :-)

I definitely agree that well defined languages (which you raise "the ill-defined IO model...in many languages") are easier to program in, becuase they are easier to reason about. However that reasoning may be informal. Ie the programmer's mental model is simpler.

However, I disagree when say more testing doesn't help. For the last year of so I've been coding in an XP fashion which means testing upfront. I've found the quality of my code has vastly increased and the more tests I have the less likely it is there are remaining bugs. Maybe I'm just operating on high gain part of the slope and doing more testing won't help beyond a certain point by so far that isn't my experience.

Finally, you state "provably reliable software" which implies this is desirable. Unfortunately I've learned that bug-free software doesn't pay. There is always the tradeoff between time and quality and the point on that continuum that proven software occupies is seldom optimal. Unless proof techniques can get a heck of lot better than they currently are there isn't much value to them in day to day development.

I agree that many times informal reasoning is enough, and I am all for languages that are clean enough to make such reasoning easy.

I agree that in most day to day programming situations proving correctness isn't cost effective. My guess is that this can be helped by having better languages and tools.

On a broader (slightly off-topic) note, I can't help but think that the usefulness of computer tools in teaching technical subjects in general (especially mathematics) has been largely unrealized. Most math students learn to use Mathematica and/or Maple to do symbolic manipulations, and maybe Matlab to do number crunching, but I'd like to see computer environments become an essential element in teaching mathematics at all levels. Many students conclude that they are "not good in math" because they aren't good at doing large amounts of error-free symbol manipulation on paper (exactly what computers are good at). The Beseme project is interesting precisely because it uses computer languages to facilitate learning in an area of mathematics where traditional computer algebra environments are less useful (proofs).

I can think of a few examples where testing doesn't cut it, in addition to Ehud's example of security. A classic example is concurrency, where testing often doesn't show rare race conditions. With a formal calculus of concurrency (say, CSP, maybe the pi-calculus?) you could prove a program free of race conditions. Erlang (which I suspect Luke can tell us a bit about ;) is based on CSP. Another example that comes to mind is the data mining software I develop at work. This sort of program is designed to extract interesting features from data. It's very hard to test (except with very simple test data) because you never know if your implementation is buggy or your data simply has no interesting features. It would be nice to be able to prove that the program is correct (ie it is equivalent to the published algorithm). Existing FP hasn't tended to concentrate on numerics so this area is a bit weak.

And now for something completely different...

I see XP in part as a reaction to the onerous heavyweight processes of Rational UP and the ilk. However I think XP is more than a reaction to RUP; it is as much philosophy as methodology. To accept XP you have to take a very open and flexible approach to life, which naturally doesn't suit some people. No doubt all methodologies have their associated culture/philosophy but I don't see this as clearly as I do with XP. The XP maxim "do the simplest thing that could work" is _all_ about aesthetic decisions: beauty and craftmanship! When did you last see that mentioned in a Rational tome? This is interesting to me. I'm not sure why yet, but I think it ties in to ideas about creativity and skill mastery. People who have mastered a skill use that skill intuitively and are often unable to explain why they do things the way they do. XP seems to be pushing one to operate at this level, where decisions are intuitive. It's kinda a Zen philosophy to programming - don't think, just react to the code.

Does that make sense?! :)

Of the XP principles I am esp. fond of refactoring and the emphsis on unit testing. I don't think that unit tests should replace typing, nor do I think refactoring should replace design. But I do think these are useful techniques that are well worth using.

To make this a liitle more on topic for LtU: The Refactoring Browser is an interesting programming tool.

A simple example: Imperative languages that don't allow you to mess with the for loop counter variable are easier to reason about. When you come across a for loop you can tell how many iterations are going to occur etc. This is good for understanding; it also makes the proof rule easier to formulate and use.

C style for loops are thus in some sense harder to reason about.