Lambda the Ultimate

The way to teach it, in our view, is to start with concepts. Not syntax or semantics or some particular programming language. (I like the phrase that Matthias Felleisen uses about his book "How To Design Programs": to "abolish the tyranny of syntax".)

Start with a small set of concepts and design principles. Then add concepts one by one and update the design principles accordingly. Each new concept has to be motivated: it has to simplify programs. (This is what I call the "creative extension principle" in CTM.)

Applying this approach coherently is not easy, since most existing languages can't go very far along this path (they don't have many cleanly separated concepts). E.g., the Tucker and Noonan book "Programming Languages: Principles and Paradigms" does an heroic attempt, but it does not have the research results to back it up. For CTM we were lucky to have a lot of research to back us up (actually, that is why we originally decided to do the book).

The concepts-based approach can lead to nonintuitive paths to teaching programming. For example, one could start with a simple functional language. Then what is the next concept to add? One could add state (leading to OOP). But, in what was an unexpected but happy surprise for me, one could add concurrency instead. This leads to declarative concurrency (which will be the topic of another discussion). We have successfully taught courses to second-year students following this unorthodox path.

I am going to propose a "Birds of a Feather" session at SIGCSE 2004 on the concepts-based approach and how we realize it in CTM.

Is this fair? Why or why not?

Then why the syntax of Oz as opposed to the simpler Scheme of SICP?

8^)

Regarding syntax: the "tyranny of syntax", in my view, means that older programming books tended to spend lots of time on meaningless issues related to syntax, such as whether the semicolon ';' should be a terminator or separator. It does *not* mean that syntax is not helpful for understanding! Having a uniform syntax just means that the richness of the language is pushed away from the syntax and into the names of language entities. This adds a second layer of syntax!

That's why I do not like a uniform syntax. The ability to do macros easily is not enough justification for it; rather, the language should make it easy to manipulate syntactic constructs as first-class entities. (This is a possible future research direction for Oz, to allow building linguistic abstractions in the language.)

In regard to uniform syntax: I think everybody agrees there's such thing as too little syntax and too much syntax, but where to place the line dividing the two depends wildly on what you're used to. I'm used to PLT Scheme, and I find myself thinking that the syntax is just right; I wouldn't give up quasiquote or the ability to use square brackets in place of parens, but when I program in ML or C or PHP or whatever else I get really aggravated by all the silly little rules I've got to remember just to get the compiler to parse my program correctly. On the other hand, other people argue up and down that (e.g.) C's syntax is elegant and beautiful and that Scheme just looks like one undifferentiated lump.

I guess the question is, what's actually best for students who haven't seen any PL's syntax before? And that's more a question for empirical studies by education researchers or psychologists than for computer scientists. I wonder whether anyone has actually done a study like that.

It is clear that programming in certain languages is a branch of constructive mathematics. If you program in a typed lambda-calculus, by the Curry-Howard isomorphism you are writing proofs, which is undoubtedly a mathematical activity.

It is (or should be) rather a branch of engineering

Mathematics is a successful, well-developed field. If we can leverage that knowledge for programming, why shouldn't we? Is it impossible to conceive of programming as both a mathematical and engineering activity? I can certainly think of situations in which mathematicians behave as engineers, and vice versa.

Programming is then like other engineering disciplines: a mix of back-of-the-envelope reasoning, standard techniques, and standard tools, supported by formal reasoning and empirical measurements.

This also sounds like how mathematics is done in practice.

The way to teach it, in our view, is to start with concepts.

It seems to me that this is not incompatible with the mathematical viewpoint. You can teach mathematics by starting with concepts: functions, relations, graphs, trees/terms. The advantage of employing mathematics here is that these concepts can (later, if you prefer) be rendered well-defined and that the student becomes familiarized with foundational notions that provide stepping stones into a vast, extant repository of knowledge.

In contrast, by starting with bigger concepts like `declarativeness' and `state' and `concurrency', you are only giving them an introduction via ill-defined and still-evolving terminology to what remains an immature field.

It seems to me that, at the very least, the mathematical perspective instantly establishes a connection between program correctness and the formal tools necessary for the verification of program correctness, tools for which the engineering perspective does not provide adequate alternatives.

Also if you hold that programming is an engineering discipline, you have to conceed the necessity of technicians and assemblers. The majority of what we call programmers these days are not engineers - they would fall in the technician catagory.

Programming a general-purpose application is the application of standard techniques (as is done in civil engineering, e.g., for building bridges) to achieve a result. That is, applying existing theorems, not proving new theorems. I would not say that is *doing* mathematics, but it is certainly *using* mathematics.

I do think that the engineering perspective is perfectly adequate for thinking about program correctness and formal tools. What do you think that civil engineers do when they verify the structural stability of bridges? They are applying formal methods. But I don't think you can say that they are proving new theorems.

I am at a loss to understand what you are trying to say here. Why are the three concepts you mention 'bigger'? State is a sequence of values. Concurrency is a property of a partial order. Why is this terminology ill-defined and still-evolving? Both are simple mathematical concepts that provide stepping stones into the vast repository of extant mathematical knowledge. I agree with you that this must be exploited--in the same way that, e.g., complex analysis is exploited by electronics.

I do agree that the word "declarative" has been used in many ways in the past. This is part of the historical growth of the programming field. We take some pains to explain these different ways, so the student will not be confused.

I also agree that programming is still an immature field. That's one of the reasons we wrote CTM--to help programming become mature.

What I buy is precision. It would be inaccurate to say that programmers are (or should be) mathematicians (which is what your remarks imply). On the other hand, comparing the activities of programmers to that of civil engineers or electronic engineers is accurate.

As I explained, this in no way precludes the use of mathematics by programmers. On the contrary, as in any good engineering discipline, they will be (or should be) using a fair amount of mathematics.

How to teach CS1 is a well known problem. I change my opinion about it quite often. At the moment, I think CS1 should use some form of functional programming, and discuss proving correctness and (semi-)formal models as soon as possible. I don't really care if GUIs are not discussed. HTDP looks like a good candidate at first look, but I really don't like the emphasis on design (and design recepies). I think CS1 is too early. I want to cultivate more fundamental reasoning skills. I think thats the way to achieve the goals the authors say they are trying to achieve, goal I agree with whole heartedly.

When it comes to software engineering, I am less sure. I think the field is far to immature, and no approach seems like a good idea at the moment. Maybe software engineering will never mature, I don't know (well, I have my opinion, but that's another topic, so I'll leave it aside for the time being). We need to rely on programming knowledge, whether it is organized nicely (like in CTM) or not, but focus our attention not on "programming" but on "design" is its widest sense, using techniques from all languages, and also ideas that are not directly implemented at the moment in any widely used language (like AOP was a few years ago). Of course, we should choose programming languages that offer useful constructs, and use them to build things that actually work. But most importantly we need to encourage critical thinking skills, analysis techniques (which include quantative tools, logical thought, verbal argument and the like). The goal being to prepare students to separate the wheat from the chaff, seeing as most arguments regarding software engineering cannot be backed by solid evidence or sound logic.

When the situation changes, we will need to change the didactic approach. At the moment these critical skills are essential...

Answering everyone generally, no one in particular:

Perhaps some analogies will elucidate Frank's remarks. Think about airplanes. The heroes of old were seat-of-the-pants pilots who knew a craft's performance by vague and ill-defined metrics: a certain hum, a particular vibration. That is where we are today in programming. We have slow airplanes piloted by seat-of-the-pants hackers who flatter themselves about piloting skills and swap war stories. Some, rightly so; but there is a better way to build airplanes, one that surpasses any human piloting skills; and the analogy with software engineering is almost exact.

To attain the hypersonic jet age of software, we need what hypersonic jets have: automated, mathematics-based control systems. That is where Frank wants to go. Actually everyone does, but not everyone knows it yet (excluding PVR; I mean generally).

Some of today's hyper-agile, hyper-sonic fighter jets would physically fall from the sky without computer control. Their aerodynamics are intentionally unstable so as to push the performance envelope. Bare human piloting is simply impossible. Human brains and bodies cannot respond like high speed computers executing control theory mathematics. So the human pilot of today oversees a control system built by engineers familiar with control theory and aerodynamics. What that buys is power - more speed, more agility, more survivability, more altitude. The same will be true of software systems.

This modern pilot need not, himself, be an expert in control theory. So it is with mathematics underlying future software systems. Users need not be experts. That fallacy is one of the common sticking points in discussions on the utility of mathematics. Not everyone who uses mathematics need understand it. For example I use control theory every time I set my house thermostat or drive my car in cruise control. You get the idea here, and I think that's what Frank is trying to say, in part. It's also what PVR means about software guys not doing proofs.

While I do accept PVR's comments in full, as well as Frank's (I see no conflict, just definitional semantics between them), I express a broader view, and say that the mathematics can lift all boats, not just the engineer's. The everyday driver, as it were, can use cruise control. We'll have mathematically trained software engineers designing formal software systems, and non-mathematical programmers using them. These systems won't be able to solve every problem in hands-off fashion, but neither do they need to (that's just another fallacy). In effect they'll give programmers the software equivalent of a fighter jet yoke. They won't replace the pilot, just give him more power. What the programmer does with it is up to him.

Perhaps the converse notion is worth consideration: that programming can influence mathematics. I'm not sure it's quite exactly his thesis, but Stephen Wolfram's book, A New Kind of Science, goes far into that territory. As the primary author of Mathematica and a Ph.D. physicist, this man certainly understands mathematics. So it's curious that he would adopt the viewpoint of programs as more fundamental descriptors of nature. I'm not trying to agree with him (not at all, one way or the other), just pointing out that the traffic between mathematics and programming may be more complex than we know yet.

" Gerry Sussman's keynote was awe inspiring. Having had my brain blown by SICP I was very excited by the prospect of attending his presentation and I was not disappointed. Sussman's passion these days is teaching and that was obvious from his talk. Sussman contends that the greatest achievement of 20th century computer science is not the computer or the network.

Instead he argues that the development of languages that can be used to precisely specify processes or algorithms is of greater significance. In their efforts to devise notations that can be used to explain computers how to do things like square roots or Lagrange equations, Computer Scientists ended up creating new kinds of languages for human expression. Such languages happen to be executable by machines, but Gerry feels this is of secondary importance compared to their use as tools for precise human reasoning and communication, particularly in teaching.

He has investigated this insight while teaching classical mechanics at MIT. The idea of programming languages in general and Scheme in particular as tools for expressing processes was already present in SICP and seems to be further explored in Gerry's new book, 'Structure and Interpretation of Classical Mechanics'."

Some of the techniques are standard, certainly; but in every application there are some novel techniques which must be applied. Otherwise, surely we could automate the process...?

That is, applying existing theorems, not proving new theorems. I would not say that is *doing* mathematics, but it is certainly *using* mathematics.

I really don't see how you can reconcile the fact that writing a function of type A -> B is the same as writing proof that A implies B with the claim that programming is not a mathematical activity. If proof is not mathematical, what is?

I do think that the engineering perspective is perfectly adequate for thinking about program correctness and formal tools. What do you think that civil engineers do when they verify the structural stability of bridges? They are applying formal methods.

There are two differences between verifying the safety of bridges and the correctness of programs.

First, engineers have access to a set of tools which allow them to quantify and empirically compare the error tolerance in their designs and the actual, measured error in their products. Programmers don't. You can run tests on a program, sure, but that does not let us compare tolerance with measured error since we have no notion of error `distance' between specification and implementation.

Second, programmers have, potentially at least, access to a set of tools which engineers do not, namely, formal (mathematical) verification of implementation against specification. This is a technique which engineers cannot apply; while you can prove that a bridge design is safe, you cannot prove that a bridge itself is. In contrast, it is possible to prove the correctness of an program implementation w.r.t. a specification.

I am at a loss to understand what you are trying to say here. Why are the three concepts you mention 'bigger'? State is a sequence of values. Concurrency is a property of a partial order. Why is this terminology ill-defined and still-evolving?

If you had asked me to define `state', I might have said number of things which are more or less general than, and perhaps incompatible with, the definition you gave. For example, I might observe that one needs to impose some notion of irreversibility, to avoid so-called `snapback'. That calls for extra structure. Or I might demand that `state' include and perhaps distinguish read and write operations. Or I might demand that state include a notion of locality and interference. If you ask other researchers, I think you would also get a range of opinions. For concurrency doubtless even more.

If you really believe that `state' is just a sequence of values, then why bother with the word anyway? Why not just say `a sequence of values'? It seems to me that by using the word `state' you are trying to encompass a number of distinct notions. There's nothing wrong with that, of course, but I think this does substantiate my point that these words are indeed ill-defined and still-evolving.

What I buy is precision. It would be inaccurate to say that programmers are (or should be) mathematicians (which is what your remarks imply). On the other hand, comparing the activities of programmers to that of civil engineers or electronic engineers is accurate.

While I agree there is a perception that mathematicians are researchers and engineers are not, and that in this regard programmers are more like the latter, I find it difficult to overlook the Curry-Howard correspondence which precisely frames programming as a mathematical activity; also note there is no similar correspondence in the world of engineering. Not only that, but I think my remarks above about two differences between bridge-building and programming also point in the other direction: there are facets to programming which are shared by mathematical activities and not by engineering activities.

I agree with your comments on state. It is a word that has been given different meanings, due to the immaturity of the field. But this is irrelevant, since in CTM I give it a precise definition, so the students are not confused. This is part of the maturation of the field of programming, giving precise definitions to basic concepts.

First, engineers have access to a set of tools which allow them to quantify and empirically compare the error tolerance in their designs and the actual, measured error in their products. Programmers don't. You can run tests on a program, sure, but that does not let us compare tolerance with measured error since we have no notion of error `distance' between specification and implementation.

I disagree. Both programmers and other engineers have (1) tools that allow them to measure simple properties (like physical size, memory usage, ...) and (2) tools that allow them to investigate some more complex properties (like liveness of protocols, stability of bridges, ...). The fact whether the properties being measured are linear or nonlinear functions of the spec. has nothing to do with it.

(...) while you can prove that a bridge design is safe, you cannot prove that a bridge itself is. In contrast, it is possible to prove the correctness of an program implementation w.r.t. a specification.

Absolutely not! A program implementation is a hardware/software combination that relies on the laws of physics. How can you pretend to prove its correctness?

A final point: the distinction between hardware and software is a gradual one. In the final analysis, what's the difference between a program running on a computer, an electronic circuit, and a mechanical device to solve the same problem? All are artefacts that use physical law to solve some problem, e.g., they could be solving differential equations.

By this reasoning, blowing soap bubbles in wire frames is a mathematical activity: you are solving a series of complex partial differential equations.

The Curry-Howard correspondence is a technical statement about lambda calculus, not a statement about how programmers build their artefacts. How or why should this technical statement affect the lives of programmers?

It reminds me of one of Molière's plays, where one of the characters is astounded to find out that he has been saying prose all his life.

Remember this story about Feynman?

Richard had completed his analysis of the behavior of the router, and much to our surprise and amusement, he presented his answer in the form of a set of partial differential equations. To a physicist this may seem natural, but to a computer designer, treating a set of boolean circuits as a continuous, differentiable system is a bit strange. Feynman's router equations were in terms of variables representing continuous quantities such as "the average number of 1 bits in a message address." I was much more accustomed to seeing analysis in terms of inductive proof and case analysis than taking the derivative of "the number of 1's" with respect to time. Our discrete analysis said we needed seven buffers per chip; Feynman's equations suggested that we only needed five. We decided to play it safe and ignore Feynman.

OK, but I think it's relevant for clarifying what you regard as the essence of a `concept-based' approach. To me, the `concept' of state is broader than any particular formal definition of it. You just said that you choose a particular definition; so what is conceptual about your approach?

Both programmers and other engineers have (1) tools that allow them to measure simple properties (like physical size, memory usage, ...) and (2) tools that allow them to investigate some more complex properties (like liveness of protocols, stability of bridges, ...). The fact whether the properties being measured are linear or nonlinear functions of the spec. has nothing to do with it.

I don't deny that programmers have tools for measuring properties of programs. What I'm trying to point out, rather, is that the theory which supports the exploitation and interpretation of data gathered by those tools is completely inadequate.

For example, say I write a program which is intended to conform to some spec. To investigate its correctness, I design a testing suite and run my implementation on a million tests. So, now, what have I learned? Can I say my program is 10%, 50%, 90% correct? How am I to interpret the results of my testing? There is some theory about this, coverage and so on, but it's not much, and hardly ever used in practice. And when it is used in practice, the other half of the equation is not balanced: using coverage or something, we may be able to measured the observed error, but in practice specs do not say anything about how much error can be tolerated.

I think this situation is very different from that in engineering circles, where such concepts are well understood and ubiquitously applied.

(I don't know what you think nonlinearity has to do with it.)

A program implementation is a hardware/software combination that relies on the laws of physics. How can you pretend to prove its correctness?

I can take the correctness of the underlying platform as a hypothesis and prove its correctness w.r.t. to the platform's specification. If the platform is malfunctioning, that's not the programmer's problem, surely!

In the final analysis, what's the difference between a program running on a computer, an electronic circuit, and a mechanical device to solve the same problem?

There is a world of difference: computers are digital and consequently produce exact results. How many millions of man-hours have computer engineers expended to ensure this property? Why shouldn't we exploit it? Surely it's a waste not to.

Why should I, as a programmer, have to fumble around with error tolerances when I can get an exact result? Why should I, as a consumer and user of programs, have to tolerate errors (no pun intended) when it is within the ability of programmers and the capabilities of the platform to produce exact, provably correct results? If I want to see fuzzy images, I'll buy a TV; if I buy a computer, I bloody well want every pixel in the right place.

This is a comment on the state of the art, not on whether programming is an engineering discipline. I agree with you on this one.

I can take the correctness of the underlying platform as a hypothesis and prove its correctness w.r.t. to the platform's specification. If the platform is malfunctioning, that's not the programmer's problem, surely!

All engineers do this. For example, an electronics engineer can prove the correctness of an electronic circuit (within tolerances that he can calculate), taking the correctness of the basic components as a hypothesis. His calculations confirming the correctness, whether done manually or with SPICE, can be considered as a mathematical proof.

Why should I, as a programmer, have to fumble around with error tolerances when I can get an exact result? Why should I, as a consumer and user of programs, have to tolerate errors (no pun intended) when it is within the ability of programmers and the capabilities of the platform to produce exact, provably correct results? If I want to see fuzzy images, I'll buy a TV; if I buy a computer, I bloody well want every pixel in the right place.

Actually, I agree with you on this (modulo a minor comment to be made below). But again, this comment is on the state of the art, not on whether programming is an engineering discipline.

The minor comment: sometimes error tolerances are unavoidable, even in the exact world of digital calculation. This is often due to resource limitations (speed limitations of a CPU in arithmetic, for example) but can be inherent (some problems are ill-conditioned and even the best programs can't get around that). In a famous article, Edgar Allan Poe dismissed Von Klemperer's chess-playing machine partly on the grounds that a mechanical device would necessarily play perfectly, and yet the chess-playing machine sometimes lost. Now we know better: there are sound algorithmic reasons why a chess-playing machine will not play perfectly with the computing power at our disposal.

Surely not: when I do mathematics via Curry-Howard, I am producing a proof, a physical artifact which can be inspected and verified by my peers. In blowing a soap bubble, I may be solving equations, but I am not producing a proof, some objectively certifiable artifact that shows I correctly solved them.

The Curry-Howard correspondence is a technical statement about lambda calculus, not a statement about how programmers build their artefacts. How or why should this technical statement affect the lives of programmers?

I could counter this in a number of ways, but the simplest is: engineers employ many technical statements (about their tools) in their work. For example, `this crane can only support so-many tons' and so on. Why shouldn't programmers?

It reminds me of one of Molière's plays, where one of the characters is astounded to find out that he has been saying prose all his life.

haha Well, I think there is no more reason to be downcast about the fact that you've unknowingly been doing mathematics your entire professional life than there is about the fact that you've unknowingly been writing prose. Being able to see things from multiple perspectives is never a hindrance, and, when one perspective gives a great deal of context to exploit, as is the case with the mathematical perspective, it can be a great help. Sometimes even the solution to a problem you would not otherwise have been able to solve...

There is a difference: an engineer can prove correctness of the design of a circuit, assuming correctness of its components. But the design is not the product; it's not what ships. (Hm, unless you distinguish engineer from manufacturer...) The correctness of the product itself can at best be measured empirically, and never proven. A programmer, though, can prove correctness of the product itself, the thing that ships, since a program is a formal object.

sometimes error tolerances are unavoidable, even in the exact world of digital calculation.

Yes, I'm aware of this; I only say that we should exploit discreteness when possible.

You have hit on a crucial point. This is the essential difference between programming and other engineering disciplines: programming is as close as you can get to building artifacts in a purely formal realm. Our raw materials are not metal or plastic, but entities that behave like Platonic mathematical concepts. Still, we are engineers in this ethereal domain. We use it to build real artifacts that solve real problems! Now how would Plato feel about that?

But we don't sell pure information. Programs have to be encoded in some medium and distributed. Using digital encoding mechanisms raises the barrier to entropy, but does not eradicate it. It is perfectly possible (albeit highly unlikely), that you will ship your correct Haskell code to me on CD, but that I will read into my computer a Visual Basic program complete with mandatory bugs, or that the CD will suddenly shift-shape to become a small model of the Eiffel tower.

The difference is one of degree, of probabilities. You can argue that the numerical differences are large, but I'm not sure that is as important as knowing what the probabilities are. Maybe an engineer that knows 1 in 1000 of the instances produced fails, in agreement with requirements, is close to your ideal mathematician-programmer. While the engineer responsible for a product that fails much more than expected (or, alternatively, fails much less, but is too expensive) is closer to those mortals amongst us who write code that needs testing.

Why should an engineering product be necessarily physical?

"[...] We decided to play it safe and ignore Feynman."

But neglected to include the important bit further on in the cited piece:

"The decision to ignore Feynman's analysis was made in September, but by next spring we were up against a wall. The chips that we had designed were slightly too big to manufacture and the only way to solve the problem was to cut the number of buffers per chip back to five. Since Feynman's equations claimed we could do this safely, his unconventional methods of analysis started looking better and better to us. We decided to go ahead and make the chips with the smaller number of buffers.

"Fortunately, he was right. When we put together the chips the machine worked."

I like what Frank wrote: "I think there is no more reason to be downcast about the fact that you've unknowingly been doing mathematics your entire professional life than there is about the fact that you've unknowingly been writing prose."

Programming *is* a branch of mathematics, and programs are mathematical objects (however unsatisfactory they may be as such), but I don't see how that conflicts with the idea that when practically applied, it is also a matter of engineering. Isn't any practical application of any formal discipline, essentially engineering? (I'll have to ask my dental engineer what he thinks about that when I next see him.)

Should programming be taught the same way math is being taught?

Or should math be taught more like programming?

I am not impressed overall with math education in K-12 in the US.

There is a difference: an engineer can prove correctness of the design of a circuit, assuming correctness of its components. But the design is not the product; it's not what ships. (Hm, unless you distinguish engineer from manufacturer...) The correctness of the product itself can at best be measured empirically, and never proven. A programmer, though, can prove correctness of the product itself, the thing that ships, since a program is a formal object.

I can take the correctness of the underlying platform as a hypothesis and prove its correctness w.r.t. to the platform's specification. If the platform is malfunctioning, that's not the programmer's problem, surely!

Also, just because a program is "correct" does not mean that it performs adequately.

But most importantly, what is this thing you call a specification? How often do you actually have one that is precise enough for you to prove? Almost never. Even in fields, such as telecommunications, where formal specifications are (sometimes) used, you still need to test to verify that everyting works. Specifications have bugs, too, and always will.

1) I have an acquaintance who researches the properties of hydrogen (including, for this illustration, its conductivity). 2) I have another acquaintance who designs circuit boards for custom computing hardware. 3) I had a nice conversation with the person who installed my cable TV and broadband access. 4) I don't know anyone who works on an assembly line in a factory owned by Sanyubishirola, but know that these folks exist.

All of them are engaged in a field we could call "electronics" but one does so as a scientist, one as an engineer, and two as technicians. At first-order approximation, I see these three levels as follows:

1) "scientific" activity as the search for fundamental knowledge; 2) "engineering" activity as the application of that knowledge (and a heritage of experience) to solving practical problems; 3) "technical" activity as the routinized production, deployment, and service of such solutions.

Likewise, I regard "programming" as an area of human activity that cuts across many layers such as the above, with computing science and mathematics at one extreme, and routine coding at the other; this leads me to regard "Programming is/isn't mathematics" in the same light as "Tuesday is/isn't 8:00 AM".

Serves me right for sounding too dogmatic, now I have to explain myself.

My base claim here would be that programs are mathematical objects. Sure, practical programs have all sorts of hairy connections relating to grungy real-world things, but this is all embedded in something which can be reduced to one of the mathematical models of computation.

If you accept that programs are mathematical objects - no matter how undisciplined they may be in their construction or expression - then you must accept that the end result of the activity of programming is a mathematical object. In this sense, at least, programming *is* a branch of mathematics - whatever else it may be, or overlap with.

There are certainly things involved with the act of programming which we don't think of as mathematics, and many of those things we do think of as engineering, particularly for certain kinds of systems. But I don't see it as quite correct to say that programming is a branch of engineering, because it is possible to write programs without applying engineering principles - and many people do!

In writing such programs, engineering is not being done, but assuming a working end result is achieved, it is still something recognizably mathematical. You can say these programs are poor mathematics, but they're still fundamentally mathematical. You can't say that they're fundamentally works of engineering, because engineering in the sense discussed here implies some attempt to apply knowledge in a disciplined way. Not all created products are engineered. So I'm saying that in programming, you can avoid engineering, wilfully or otherwise, but you can't avoid mathematics.

But I agree that the engineering aspect of programming needs to be taught. OTOH, I think the mathematical aspect is still under-represented - the advances in formal computing science of the last half-century have not trickled down to every college - so I see some benefit in emphasizing the mathematical aspect of programming, for the foreseeable future (although, of course, that may turn some people off).

On teaching: I notice that in the current ACM SIGPLAN notices, which are the proceedings of ICFP '03, there's a paper by by Rex L Page, "Software is Discrete Mathematics":

A three-year study collected information bearing on the question of whether studying mathematics improves programming skills.

More on teaching: Patrick provided a quote about Sussmann's ILC '03 keynote. Sussmann's broadest theme, of using a mathematically-inspired computational approach for teaching and understanding, was echoed in at least three other people's talks, which may not be much news to LtU readers: Matthias Felleisen, Philip Wadler, and Gregory Chaitin. Felleisen uses this approach to teach programming, of course (the TeachScheme! project); Wadler thinks that both God and space aliens program in typed lambda calculi; and Chaitin enjoys developing computations to prove fundamental truths.

A common theme which I think can be extracted here, and which these talks addressed either implicitly or explicitly, is that a mathematical/computational approach to both thinking and teaching has benefits which haven't even begun to be widely appreciated or exploited. Felleisen argues that this includes the teaching of programming.

Yes. This accords with my view that calling programming a mathematical activity does not necessarily imply that programmers must be researchers. Perhaps we can compromise and call programming `mathematical engineering'.

Andrew: But we don't sell pure information. Programs have to be encoded in some medium and distributed.

I don't find this particularly convincing, but I think a better argument along this line could be made by pointing to runtime/environmental dependencies of non-trivial programs. But I'm not going to argue against myself. :)

Ken: Ummmmm, yeah, right. Remind me not to hire you.

No problem. Same to you.

Also, just because a program is "correct" does not mean that it performs adequately.

It does when `performs adequately' is mentioned in the spec.

But most importantly, what is this thing you call a specification? How often do you actually have one that is precise enough for you to prove? Almost never.

If, by `you', you mean me: the non-trivial software which I write does generally have specs rigorous enough to verify implementations. For example, recently I proved the correctness of a Haskell-XML data binding w.r.t. a formal semantics of XML Schema. I didn't prove correctness of the actual implementation, admittedly, but rather the translation algorithm itself. IMO, the fact that proving correctness of the implementation itself is impractical is a hole in the tools available for Haskell, but not an insurmountable one. At least I eat some of my own dogfood.

If, by `you', you mean `software developers in general': I dunno, though I expect it's not often that they develop rigorous specs. But then, just because they don't, doesn't mean they shouldn't. In particular, I do believe that at least the core of a system should be specified semi-rigorously, and that it is not impractical to do so.

Even in fields, such as telecommunications, where formal specifications are (sometimes) used, you still need to test to verify that everyting works.

Did I say otherwise? I guess you imagine that a mathematical approach to programming precludes ever running the program. Does the engineering approach preclude ever employing mathematical proof?

Specifications have bugs, too, and always will.

So we should throw the baby out with the bathwater? And I thought nihilism was dead.

Joel: At the risk of sounding like a contrarian, I'm very skeptical of *any* sentence of the forms "X is Y" or "X is not Y"

The point of calling programming a mathematical or engineering activity is not to pigeonhole it, but rather put it in context and enable the transfer of ideas across disciplines. IMO, there is too much of a sense in the programming community that programming, and indeed IT in general, is just something so completely mind-bogglingly new that we might as well develop it from first principles.