Lambda the Ultimate

People who derive economic benefit from programming do not want correct programs. They want their programs completed sooner, at less cost, with more (imperfect) features. Their policies and processes are designed to release programs with known bugs which are also expected to ontain even more undiscovered bugs.

As a theoretician, I'm agast; as a practitioner, it all seems perfectly reasonable. In fact, I'd like to see programming languages explictly include debugging features just as I like it when processors include debugging capabilities.

-- Vladimir

Care to elaborate, or will this spoil the troll?

Well, a bit more seriously, I think that it would help to have language support for pervasive range and bounds checking with as much being done at compile time as possible, the rest being left to run time with an option to leave it out altogether in order to improve efficiency.

One of the greatest difficulties with fixing bugs is finding where they are rooted (oh-oh, mixed metaphor, I guess I should be calling them "weeds" and not "bugs" if I think they have "roots"), so language support for early discovery when things go awry is a good thing. On the other hand, if the language features are too cumbersome and heavy, then they won't get used and the feature is moot-- always a balance!

In this regard, MS Excel has a helpful debugging feature in which it draws the dependency graph for a particular cell on top of your spreadsheet. If nothing else, this allows you to limit the scope of your search for the problem. A general purpose language which allowed you to walk the dependency graph in some manner when things go awry might be useful.

Walking the dependency graph seems like an IDE feture, not something the language can (or should) provide.

These kinds of things are possible in languages that have reflection, e.g. Smalltalk, Lisp, Java, C#. For other languages you have to build a parser, add the semantic analysis, etc.

The original Smalltalk refactoring browser uses this information to analyze and automate source-to-source code transformations. The problem with Java and C# with refactoring is the objects only exist "at run time" not during development. And so even though they "have reflection" it cannot be used very well for development-time tools. Each vendor of these tools does the "write the parser, add the semantics" song and dance all over again.

My initial conclusion was probably somewhat fed by the fact that McCarthy's own descriptions of the invention of LISP emphasize his attempts to address mathematical issues of computability from the perspective of function application - something Church had already done, more comprehensively and correctly, decades earlier. In addition, although McCarthy used 'lambda' as a keyword in LISP, he apparently used more it as a notational device, without familiarity with Church's calculus, and this showed clearly in the design (and shortcomings!) of LISP. There's some discussion of this here:

This leads to the question of McCarthy's knowledge of the lambda-calculus. McCarthy always pointed out that he did not know much about this. It is obvious that he has read the first pages of Church's paper [C41]. The 'eval' of March 1958 proves that he did know about substitution. However, there is no sign of renaming variables, no sign of normalization. One cannot believe that McCarthy did not study carefully the substitution procedures of the lambda-calculus for his realization, but this is the only explanation for a series of errors that were not apparent in the simple examples of 1958. Today, we all know much better.

I thought perhaps McCarthy still hadn't gotten around to reading Church... ;)

Of course, as it turns out, being from 1962, this paper was rather prescient. I notice it is cited by people like Milner in subsequent papers about denotational semantics.

The number of real-world programming methodologies that don't use debugging is precisely zero. This, it seems to me, is a powerful argument that there is no value in being able to prove programs correct.

The number of real-world programming methodologies that produce correct programs is precisely zero. This, it seems to me, is a powerful argument that there is no value in being able to debug programs.

People who derive economic benefit from programming do not want correct programs. They want their programs completed sooner, at less cost, with more (imperfect) features. Their policies and processes are designed to release programs with known bugs which are also expected to [c]ontain even more undiscovered bugs.

People who derive economic benefit from using software do not want incorrect software. They don't want to fiddle with buggy programs, file bug reports or contact customer service; they want to get real work done, sooner and at less cost. Their policies and processes are built on the assumption that the software they purchase actually does what the seller claims it does and it's a damn shame that they don't sue the pants off incompetent and even willfully negligent software manufacturers when it doesn't.

As a theoretician, I'm agast; as a practitioner, it all seems perfectly reasonable. In fact, I'd like to see programming languages explictly include debugging features just as I like it when processors include debugging capabilities.

As a practitioner, I'm aghast: writing correct software is harder than I thought, and I thought my customers would be more forgiving about my mistakes, even though I take their money. As a theoretician, it all seems perfectly reasonable. In fact, I'd like to see programming languages explicitly include features which help me prove my programs correct, just as I like it when physics and mathematics textbooks actually support their own claims with evidence and proofs.

BTW, Frank, I think you should begin work on a calculus of message postings so that in future, at least some of us will be able to prove our own postings correct, thus radically simplifying many of these discussions!

V {postings by Frank} E {truth}

The pattern I've seen informally looking at the research are factors like 1:2:40. For each line of program code, you need 2 lines of specification code, and 40 lines of proof code.

The end result is that it's easier to eyeball your program and guess that it's probably correct, than to eyeball the proposition being proved and guess that it's probably proving the right thing. So, as far as shipping quality code is concerned, you get 40X better cost/benefit from writing code than from trying to prove stuff about it.

Proof techniques would need to come a very, very long way before this situation changes.

When one moves to considering other kinds of software, such as software that is used to control devices (especially devices like airplanes and medical machinery), one sees a very different perspective!

You may be able to fix the bugs in MS Word in a service pack; you can't fix them in an airliner that way. You're just not allowed to crash a bunch of planes to collect the bug reports!

[oops, example from different thread, but you get my drift, I hope.]

An interesting quote:

However, there are few debuggers or profilers for strict languages, perhaps because constructing them is not perceived as research. That is a shame, since such tools are sorely needed, and there remains much of interest to learn about their construction and use.
Constructing debuggers and profilers for lazy lan­guages is recognized as difficult. Fortunately, there have been great strides in profiler research, and most imple­mentations of Haskell are now accompanied by usable time and space profiling tools. But the slow rate of progress on debuggers for lazy languages makes us researchers look, well, lazy.
"Why no one uses functional languages" 1998