Lambda the Ultimate

w/out Linear Algebra or Partial Differential Equations, it's kinda hard to do real non-pl work...

If you do graphics or engineering/simulation work maybe.

My feeling is that, in general, programmers would benefit from less calculus and more abstract algebra and category theory.

This is more the maths I was thinking of. However, I was also thinking of more applied mathematics, such as process calculi, temporal logics, and the like.

It's not about the practice.

How would you want to treat CS in a mathematical way?
Sure, there's formal semantics of programming languages, but that's a field that 95% of CS people haven't even heard of (and they wouldn't like it, either)!

Programming is about programming, software development. There is nothing about this that can be treated scientifically.

These are my reasons for considering CS as a craft. They were also my reasons for going into CS in the first place (although I don't mind formal semantics once in a while).

Produce a physical product and the sensors will detect the most minor of defects. Talk on the phone for a living, the computer will quantify your efficiency in incident response. etc. etc. etc... I've always wondered whether programming was a response to keep ahead of the machine, in an effort to be beyond reproach.

Personally I think the mistake is to confuse the question of creativity and craft which is inherently subjective, with verifiability and testability which are objective. For all we know, the mathematicians and the engineers are in the backroom getting high thinking of creative ways to view and create things. We don't really care how they go about doing things, we are just interested in objective results.

The answer is not quash creativity and craft. The answer is to require an end result which is testable. I think the discussions on art vs. math needs to concentrate on end results, rather than what is an inherently artful in the process of creation.

Getting my BS in Electrical Engineering has been highly instructive. One of the most interesting phenomena I've noticed is that most Software Engineers refer to other kinds of engineering as some kind of holy grail to be achieved.

Of course, my perception may be limited, but none of the "real" engineers around here are any better at designing things than the Software people. Heck, there are very large books full of "stock" designs, which ME's and EE's look at.

I think another way of dividing what you're saying is Analysis and Design. Design is the creative part of the process. Analysis is where you figure out whether the details are right or wrong. Sure, design has a lot to do with a "liberal arts" style education, but analysis is pure math and science.

Back to the original topic. A lot of "business" programs may not seem that mathematical, but most of the CSC people I know have serious fuzzy thinking problems from not taking enough Math or Engineering style courses where fuzzy thinking is banished to the corners.

Of course they all think Math is Calculus, which is wrong too. Proofs, modern algebra, graph theory, combinatorics are all much better suited to a CSC curriculum than an "engineering" style sequence of Calculus and Differential Equations. But then again, most of our CSC majors here want to make games, so alas, they must take both sets of Math classes :)

You're wrong - for example a treatment of mutual exclusion techniques and concurrency is pretty important if you want a programmer to write a threaded programme that doesn't deadlock.

• Automata theory and computability
• Logic and proof methods (e.g. predicate calculus and higher-order logics, temporal logics)
• Lambda calculus
• Formal language semantics
• Concurrency theories (e.g. CCS or CSP)
• Graph theory

IMHO CS should be about developing these, and other, mathematical constructs. Proving useful results about them. Finding mappings between these constructs and real programming languages and specification methods. CS shouldn't be about learning how to program Java (or the latest language of the week) or how to be a DBA (although those things might form part of the overall course of study).

Software engineering should be about taking the mathematical tools supplied by the CS community, and applying them to solve real problems. When I design a control system, I use transform theory and linear algebra, and a host of other mathematical tools, as well as the theories of dynamics developed by physicists. It's the same when I'm designing an analog circuit - there're a host of mathematical tools and theories to call on. Nothing like that appears to happen in the software world, except in limited instances. It should happen more often.

Yes, as someone else in this thread pointed out, "real" engineers often have canned solutions sitting around. But those canned solutions came from earlier work by engineers who did use theory. And the fact that they can be composed into new designs is largely due to their strong theoretical foundations. Furthermore, even "real" engineers need to know enough math and theory to analyze their new designs (disclosure: my background is in EE and aerospace engineering, so I am intimately familiar with what "real" engineers do).

CS isn't a craft. It also isn't just programming. In fact, it's not really about programming at all - a fact that (IIRC) Dijkstra pointed out decades ago.

Programming may be a craft. But it shouldn't be when it comes to large critical applications. I may "craft" a doghouse for my backyard. I'm not going to "craft" a 50-floor office building, I'm going to "engineer" it. Developing software should be treated in the same way.

Nonetheless, I would say that what is done in Computer Science departments falls under at least four headings:

1. Formal science: mostly, computer science is about programming, and what programmers need to know about the behaviour of their programming appears in principle to be describable formally. Hence the largest part of computer science is, or should be, formal science;
2. There's more to system construction than falls under the formal science part; this part, including the study of security and the study of human factors, is an engineering science;
3. Learning to program can be thought of as a liberal art; this view permeates the motivation of SICP, for example.
4. Finally, while computer science is mostly built on formal foundations, the need for some physics is inelimnable. Hence a small part of computer science studies computation as a physical process.

And if philosophy is not relevant to what we do, why do we get PhD degrees and not CSD? :)

Me, I got a DPhil.

Impressive things can happen when you encounter a philosopher who is adamant that his theories be testable. I'm a great admirer of John Pollock, who is the only AI researcher I know of who is approaching the subject from a "theory of rationality" perspective, and the only philosopher I know of who is actually building a system based on his theory of rationality. The only unfortunate thing in all of this is that his system, OSCAR, is patent-encumbered, but as always with the patent issue, I'm of two minds about it. Regardless, his How to Build a Person: A Prolegomenon and Cognitive Carpentry: A Blueprint for How to Build a Person are must reads, and it looks like "Thinking about Acting: Logical Foundations for Rational Decision Making," from his publications page, will be also.

I notice that he makes his Lisp code avaialble for research and educational use. The code is downloadable from the OSCAR page.

Why do all these aspects of commercial software production need to be identified with programming itself?

Specialization is a hallmark of mature fields, just as separation of concerns is a hallmark of good programs. Expecting one person to be simultaneously a competent programmer, artist, marketer, business executive and customer liaison is not only unrealistic, but seems more likely to encourage mediocrity or worse in all these roles.

I've already encountered many people who use the bogeyman of "changing requirements" as an excuse to disregard the problem of program correctness entirely; someone even once told me with a straight face that there is no such thing as correctness. And we have already seen one person in this thread claim that there is no rational way to approach programming at all. This is what you get when a person is trying to do things they aren't trained for or interested in. So why force them to do it? As a customer, I don't want to buy a work of art produced by a programmer, or a program produced by an artist.

Granted, with increased separation of concerns come problems of communication and workflow efficiency which are absent or easier to treat in a monolothic approach, and if we can't tackle those problems then this divide-and-conquer approach won't work. However, that doesn't mean we ought to aim for monolithism in the curriculum or textbooks. That is a completely different proposition and, I think, wholly counterproductive. It buries rather than exposes the problems that one has to deal with to produce a product.

It's been a while since Frank and I have taken a substantially different position on something. How exciting! ;-)

Specialization is a hallmark of mature fields

Well, this is true if by mature you mean "has run out of general problems". When (and if) the general problem space and solution space for software development settles into a stable patch with well-defined subareas, you may see the kind specialization you are talking about.

Right now, I think we are still struggling to solve our ever-changing problems at all.

A different way to look at it is to substitute the word "bureaucratization" for "specialization". One of the motivators for the Agile movement is that the "hey, I'm just a programmer: I don't talk to customers or design" approach just drove up costs and didn't work very effectively.

I've already encountered many people who use the bogeyman of "changing requirements" as an excuse to disregard the problem of program correctness entirely; someone even once told me with a straight face that there is no such thing as correctness.

In software development, I don't think there IS a well-defined, global notion of correctness, and for the changing requirements reason.

In order to prove correctness in a logical/mathematical domain, you need a well-defined problem in a system with fixed, known axioms.

In SD, you have a changing problem where the axioms are part of the changing parameters.

Obviously, you can still prove LOCAL correctness for some better-defined subcomponent, but global correctness is often in the eye of the beholder.

However, that doesn't mean we ought to aim for monolithism in the curriculum or textbooks.

Paradoxically, I agree very strongly here. I think I have learned more about design, real life problem solving and SD from studying math and PLT than from all the other "fuzzier" subjects I've studied.

If you pay attention to deeper patterns (what design is all about) you can learn all you need to know about design, communicating ideas with others, making trade-off decisions, etc. in a quite focused program of study.

But this requires making a distinction between "focused" and "specialized" in the sense of "good for a limited range of purposes".

What makes you think the same isn't true of other engineering disciplines? Requirements change all of the time. Projects get rescoped or decsoped. The resulting design changes ripple through the entire system. Change control boards exist for exactly that reason.

I've worked on any number of non-software projects that have been subject to serious requirements flux, particularly in the conceptual phases of the design effort. Of course, a large part of the conceptual phase involves iterating the design and requirements to converge on something feasible - whereas many software projects seem to just define a single set of requirements and then dive into coding without bothering to do any of the up-front iteration. No wonder there's so much requirements instability later in the project.

What makes you think the same isn't true of other engineering disciplines?

Nothing. I think the kind of mathematical correctness we are talking about is absent there as well. ;-)

No wonder there's so much requirements instability later in the project.

I don't think there is anything inherent in the practices of SD that are subtantially different from any other kind of engineering.

The only significant difference is customer expectation.

Customers EXPECT software to be more mutable than a building, or an assembly line, or an industrial chemical process.

Also, the kinds of goals they are trying to achieve through commissioning software are generally more abstract than most engineering processes.

Building an IC chip is concrete and can be objectively determined to work or not within given parameters.

But what if you goal is to "improve communication" or "appeal to customers" or "enhance business intelligence"? There is a huge subjective component to determining if these goals are met, or even figuring out what sort of concrete requirements they would entail.

Customers expect software projects to be able to respond to fuzzy goals quickly without a lot of capital cost, whereas when they build a more concrete product, they often have a better understanding of what is realistic (or at least understand where the money goes).

Maybe if you're talking about designing an ASIC. Not so if you're talking about designing systems directly operated by "end-users", as opposed to components.

But what if you goal is to "improve communication" or "appeal to customers" or "enhance business intelligence"? There is a huge subjective component to determining if these goals are met, or even figuring out what sort of concrete requirements they would entail.

These same problems have been plaguing systems engineers for decades. Not that they have any better solution than the software world does. But what you are describing isn't specific to software design. It's inherent in the development of many systems.

How do you move from fuzzy "wants" to hard "requirements"? How do you quantify what the customer wants? It's hard. But I'd suggest the first step is to stop trying to pretend that it's a software-only problem, and then take a look at what others have done to resolve these problems. IMHO there aren't any complete solutions out there yet. But you might start by looking at things like Quality Function Deployment (which was developed by the Japanese auto industry to help them translate fuzzy customer wants into technical requirements), Warfield's Interpretive Structure Modelling (which is intended to help unravel wickedly complex problems), or Wymore's T3SD (which provides a useful framework for considering systems in general, and how to think about trade-offs).

Customers expect software projects to be able to respond to fuzzy goals quickly without a lot of capital cost, whereas when they build a more concrete product, they often have a better understanding of what is realistic (or at least understand where the money goes).

Hah! You've obviously had different customers than I've had. Part of the design process is figuring out what the customer actually wants, because it's a good bet they don't really know. Nor do they understand what is realistic (and ofetn their ideas of "realistic" are based on extremely poor analogies with other projects they've heard of). As far as understanding where the money goes: not likely, unless the customer already has significant experience in buying the type of product in question.

If you are designing a system that is largely made up of software you will face the same problems as if you are designing a system largely made of something other than software. Unfortunately, many software "engineers" get pressed into doing more than software design (i.e. developing a program to meet a set of specs) - they are expected to do systems design as well (i.e. turning customer wants into specs). Not somethng that software "engineers" are necessarily trained for (not that there are all that many systems engineers who are good at it either - it's a hard problem). I think that it's important to differentiate between problems inherent to software design specifically, and those that are inherent to system design in general.

But you might start by looking at things like Quality Function Deployment (which was developed by the Japanese auto industry to help them translate fuzzy customer wants into technical requirements)

Some of the Agile software development methodologies have direct antecedents in Japanese manufacturing. Scrum in particular derives from such a process of the same name.

However, Scrum tends to emphasize a de-specialization of roles so that good ideas, problems and localized knowledge can better flow in the project, which seems to be different from the particular engineering lessons you may be suggesting.

Not that they have any better solution than the software world does. But what you are describing isn't specific to software design. It's inherent in the development of many systems.

I'm not sure how this contradicts my point.

To the extent that there are engineering processes that permit specialization of roles and other "heavy", specification-oriented techniques, they don't handle the mercurial customer very well.

Given mercurial customers and other unknowns, software development (or engineering in general, if you prefer) is not suceptible to being proven "correct" in advance of implementation in the way that an academic CS problem can.

We're all in the same boat if you like. Are you concerned that engineers aren't getting credit for building the boat? ;-)

Think two issues are here. One is whether the software is correct according to the customers needs. The other is whether the software is correct according to the design. That is, does the software meet the design specifications.

Now whether those specifications are fuzzy from the customers standpoint is not the same as saying the software design is fuzzy. Someone should have a very good idea of what they intended the software to do. Does the software do what it was designed to do is not always synonomous with whether it does what was intended.

One is whether the software is correct according to the customers needs. The other is whether the software is correct according to the design. That is, does the software meet the design specifications.

Let's flip this around.

There is a technique to "prove software correct": it is called testing. You can even write the tests ahead of the code. (I do.)

However, as with any engineering technique, this can only be done to specified tolerances for a specified environment. It is impossible to think of all of the real circumstances that could be thrown at a program, so it still might fail in one those circumstances, in spite of rigorous testing.

In a mathematically defined problem, you CAN completely specify the environment of the problem (the axioms of the mathematical system it is in) and prove, WITHOUT POSSIBILITY for unforseen error that a particular solution is correct.

Obviously, such mathematically results can be leveraged for particular parts of the system (eg. type checking the source, defining semantics, etc.). But it is virtually impossible to guarantee the infallibility of a whole system.

This is not neccesarilly true. For any system for which is it is possible to write a decision procedure to test if an operation is correct, it is possible to randomly test it until the desired level of confidence is achieved.

Such a decision procedure typically involves a reference implementation, but the reference implementation can remain wonderfully oblivious of any non-functional requirements, and the decision procedure can still check the non-functional requirements are met.

Of course, the bottleneck is the generation of tests, although given an appropriate formalism, specifying correct operation is relatively easy for a surprisingly large number of systems.

We have two large problems in software development:

- Understanding the customer's needs
- Ensuring the coherence of a piece of software

The first problem is open and, IMHO, falls in the wicked problem category. The second is tractable and is what most scientists think when talking about correctness. Every formal method helps solving the second problem, which is a huge benefit over what people usually do today.

Where I work, and I imagine lots of other places as well, there exists the phenomenon that QFD and other techniques for gathering customer requirements are often regarded with suspicion (or outright contempt) by programmers (many who have "software engineer" on their business card).

Many of the EEs and MEs I work with are equally derisive in their attitudes.

Part of this, I think, is Dilbertism--many technical folks are skeptical of their counterparts in marketing and management, for a variety of reasons. Another reason is that QFD and other processes are often inherently qualitative in nature, and many programmers are distrustful of processes that don't produce clear, unambiguous answers. Yet another reason is that many in the technical field have been burned (in some way or another) by fad-of-the-moment market research techniques, and are not aware of which techniques have solid study behind them and which are snake oil. (Programmers are too busy fending off the snake oil that permeates our profession, after all).

One area where programming (and much of EE) differs from the classical engineering disciplines (chemical, civil) is the nature of the customer. Civil engineers and chemical engineers don't usually deal with end-users; they mainly deal with their colleagues and with other knowledgable professionals (chemists, builders, architects, etc.). Market research, where it is done at all, is handled by other professionals (the architect in the building trades, etc). Engineers focus on translating requirements to designs.

Yet this division of labor--as mentioned elsewhere in this thread--drives many programmers crazy.

Besides, my point wasn't so much that QFD was the right tool for the job, as that the problems being described were not specific to software, and that it might pay to look at what other disciplines do. If nothing else, I think that it's important to understand which problems are unqiue to sofwtare and which are part of the larger human enterprise - you can't solve a problem without understanding the root causes of it.

BTW, it's a mistake to think that "classical engineering disciplines" get to deal with professionals who know what they're doing. I've spent some time in the space industry, and I can tell you from firsthand experience that supposedly knowledgable professional military officers are just as fuzzy when it comes to what they want from a satellite, and scientists are often hopelessly fuzzy when it comes to defining what they want from a science mission (or in understanding what is feasible, reasonable, and cost-effective). I would assume that the problems are similar fields like chemical and civil engineering.

Well, this is true if by mature you mean "has run out of general problems".

What I mean is: the more mature a field is, the more specialized it becomes.

One of the motivators for the Agile movement is that the "hey, I'm just a programmer: I don't talk to customers or design" approach just drove up costs and didn't work very effectively.

As I said in the other post, I don't really care about development methodologies, etc. except inasmuch as they make false claims about the mathematics of computation. However, the Agile "movement" (writing this I cannot help but recall a post-Columbine news broadcast which characterized goth as a "movement"), I think it is more based on "hey, I'm just a hacker: I'm afraid of dealing with correctness, so I'm not going to write a specification at all."

In software development, I don't think there IS a well-defined, global notion of correctness, and for the changing requirements reason.

Sure, there is no notion of correctness without a specification. What else is new?

The issue is not whether there is or is not a "global" notion of correctness; there isn't. The issue is whether, because the specification will evolve, we should throw out the notion altogether. Sure, it isn't easy getting onto a moving train; but getting on a moving train while closing your eyes is even harder!

Perhaps "bowel" is a better parallel?

I'm no fan of the Agile "movement", for precisely the reasons that you have described. However, I think it's a little unfair to say that they don't write specifications - in the Agile world tests are specifications. Now, they may not be good specifications (in the sense of coverage, amenability to analysis, tractability for proof etc.), but they do exist. And they are at least expressed in a formal language, so that there is (barring implementation differences in compilers) one interpretation of the spec. Certainly better than writing natural language requirements...

The other advantage of writing tests as a form of spec is that it breaks people out of the "writing requirements for the sake of writing requirements" mode, and gets thinking in terms of "what are the criteria of acceptance for the customer". Obviously, it'd be better to teach people to write good specs in the first place. But "test-driven" development is a backdoor to achieve similar results.

The issue is whether, because the specification will evolve, we should throw out the notion altogether. Sure, it isn't easy getting onto a moving train; but getting on a moving train while closing your eyes is even harder!

Strong agreement here! No one would suggest tossing out the specification process for a satellite or a building, and yet, as I've pointed out elsewhere in this thread, projects of that nature can be just as prone to requirements and specification flux as a software project. Why should software be any different?

I think it is more based on "hey, I'm just a hacker: I'm afraid of dealing with correctness, so I'm not going to write a specification at all."

My reaction to this is what you might feel if someone said: "I think goths are goths because they really want to be vampires." (To build on your analogy.)

The issue is whether, because the specification will evolve, we should throw out the notion altogether.

As Allan points out, testing is specification. I differ with him about the relative merits of paper docs though.

I've decimated whole forests writing specs (and surely will again) and I've found that tests are a BETTER form of specification, since they are objectively verifiable. ( They work or they don't. )

As to completeness and accuracy, there is NO process I have looked at (other than mathematical verification in a closed axiomatic system) to ensure complete coverage and accuracy of requirements without the intervention of human judgement.

My reaction to this is what you might feel if someone said: "I think goths are goths because they really want to be vampires." (To build on your analogy.)

They don't?

My reaction to this is what you might feel if someone said: "I think goths are goths because they really want to be vampires." (To build on your analogy.)

Aha, that's the reason I never felt like I was a goth, even if people said I was one: I never wanted to be a vampire.

The problem with using tests as specs (IMHO) is that they are designed purely for execution, and not for communication or analysis. I think that a spec should be, among other things

1. Separable from a specific implementation
2. Readable and interpretable by a person as well as a computer
3. Capable of being checked for internal consistency
4. Amenable to validation of higher-level invariants

What's the point of implementing a bunch of tests, and writing code to pass those tests, if the aggregate behavior that results from passing those tests isn't what was intended. I'd rather be able to check my specifications first, to make sure they actually imply the behavior I intend. Is human judgement still required? Sure. There's no way to avoid it in a creative endeavour. But I can use logic and math as a tool to help me apply my judgement to much larger, more complex problems.

It's much like "self documenting code," if the code is the documentation, then it does exactly what it should, always. I've read code that is full of "duh" comments, but nothing about what it all does in the end.

It's the difference between science and mathematics. In science a theory has evidence for its truth, but theories can only be proven incorrect, as opposed to mathematics where theorems can be proven correct.

So Marc is not using tests as specifications, because then any inputs not tested for have unspecified behavior, he's using tests as adherence to an unwritten/unspoken specification.

A good point, although I'd perhaps phrase it another way: a test definition can be a specification of acceptable behavior (e.g. if it includes provision for random selection of inputs - equivalent to a logical "for all"), but successful execution of a test only proves specification conformance for the input cases that have been tested. The only way to prove conformance using a test-based spec is by exhaustively testing every input (simply not possible in most situations). That is why I think that specification techniques that allow reasoning about classes of inputs are much more useful - conformance to a spec can be proved without exhaustive checking of every input case.

There's a reason that other engineering disciplines use a combination of analysis and test when developing new designs. And they often gain benefits from the fact that their systems have continuous state spaces, and therefore test results for a few inputs can be extrapolated to many possible inputs. The same is not true of software systems, which suffer from discontinuous state spaces, so we should be leaning more on analysis than other disciplines, not less.

That is why I think that specification techniques that allow reasoning about classes of inputs are much more useful - conformance to a spec can be proved without exhaustive checking of every input case.

This technique will work well for certain kinds of closed axiom systems. By all means use them for those cases.

For systems or requirements not amenable to this kind of treatment (which covers a lot of real world apps), I'm not sure how you can pull this off.

And yet "formal" methods have been successfully used on a wide variety of systems, either using proof-based verification, or mechanical state exploration of abstract specification models. So exactly which "real world apps" are not amenable to a formal approach?

I'm not saying you shouldn't test. Just that you should analyze as well. The combination will catch more errors (and different kinds of errors) than either alone. Writing a formal spec is a solid first step towards both writing test cases, and performing analysis.

I'm not saying you shouldn't test. Just that you should analyze as well.

Who could disagree with that?

Let's take this moment of enthusiastic unanimity to realize how far OT we have wandered.

I wonder if anything we've talked about could be used to build a better PL?

Tests can only validate a finite number of cases, which if used naively as specifications means you could have a program that does not behave as it should, but still pass every test.

Huh? Explain to me how you can test an infinite number of dijoint cases for arbitrary systems, and I'll gladly adopt your approach.

Heck, show me any form of specification that can rigiorously cover ALL possible situations that can arise for a general development project of ANY kind and I'll be deeply impressed.

A finite number of well-chosen tests seems to go a long way.

I've found that tests are a BETTER form of specification, since they are objectively verifiable.

...

Explain to me how you can test an infinite number of dijoint cases for arbitrary systems, and I'll gladly adopt your approach.

???

???

Not sure what your point is, but it is odd that someone advocating formal methods for SD can't make plain using ordinary logic what they mean.

As near as I can tell you seem to think that "objectively verifiable" have something to do with "infinite cases". I'm all ears for that argument.

It seems that you're the one trying to use tests to specify the behavior of your programs:

tests are a BETTER form of specification

But you're the one asking me how I can test all possible inputs:

Explain to me how you can test an infinite number of dijoint[sic] cases for arbitrary systems

So, how do you test an infinite number of disjoint cases for arbitrary systems?

At the worst you could write a data generator in Haskell and connect that to your testing framework for the arbitrary system. Is this what you meant?

--Shae Erisson - ScannedInAvian.com

dijoint[sic]

Ah, the tried and true way to lift the logical standards of online conversation: typo nitpick.

So, how do you test an infinite number of disjoint cases for arbitrary systems?

Replace the word "test" with its sensible synonym "verify" and you have a perfectly reasonable request of someone who made the claim:

Tests can only validate a finite number of cases, which if used naively as specifications means you could have a program that does not behave as it should, but still pass every test.

A reasonable person would conclude that this claim implies that there is some other method of verification that does not suffer from this limitation.

Hopefully, we are all clear, since I have nothing further to say on this overlong, OT thread, and apparently there is nothing more to hear on it either.

Heck, show me any form of specification that can rigorously cover ALL possible situations that can arise for a general development project of ANY kind and I'll be deeply impressed.

If we use proper DbC (i.e. pre/post conditions, invariants, CQS) and avoid sharing (e.g. message-passing) we can specify every single combination of states and all the valid state transitions.

I try to always use TDD but for specs DbC usually works for me without problems. We can even use formal languages (e.g. VDM-SL) with this method. IME there's not a single computable problem that can be specified with this technique.

Tests alone just don't cut it in my book. Perhaps tests embedded in a literate program would. But I still don't think you'd be able to perform the kind of verification and proof that I would like to see. Personally, I'd rather see unit-tests automatically generated from specs written in a formal spec language (such as Z or B - I won't try to argue the "readability" of these languages: how readable would a differential equation be if you hadn't been trained in calculus).

QuickCheck or Gast?

Of course, nothing is stopping one from writing a more involved verifier that uses QuickCheck annotated code as the input language.

Thanks! I hadn't seen QuickCheck before. It's an interesting idea. A little like Godefroid's Verisoft, but aimed more at sequential systems.

Automotive engineering? Aircraft engineering? Cellphone design? Desktop/laptop computer design?

The design of any system requires the determination of user wants, the translation of those wants into requirements, aesthetic design (at least for any consumer product - and often for non-consumer products as well), and may well include possibilities for mass-production or one-off design. It's called engineering (calling it "architecture" may sound more romantic - so much so that even some engineers try to call themselves "architects" now - but the end-result is the same). Is the designer of an ASIC necessarily concerned with aesthetics? No, probably not. But then neither is the designer of a library (unless it's a GUI toolkit ;)

I agree wholeheartedly with this analogy!

I think that there are many parallels between Software Development and House Building (and extending on to Community Building to parallel large software systems).

Look at how many different ways there are to build a three bed, two bath house. Look at the different ways they can turn out based on who you got to design and build. Look at how easy it is to "hang out the shingle" as a house builder.

Like it or not, programming is not simply a branch of applied mathematics.

You are conflating programming with commercial software production. I am specifically using "programming" to refer to the aspects of this process which are applied mathematics.

a full understanding of a variety of factors is fundamental to being able to produce a program that matches the requirements.

These "factors" belong in the program specification, which is ideally the only thing a programmer needs to be looking at. And yes, I write ideally to indicate that there are situations when that isn't feasible. Nevertheless, we shouldn't change our notion of what the ideal is simply because we haven't achieved it yet, or even if we never achieve it, unless we can't even make any progress toward it.

Of course, this raises the question of who writes the specification, since this is someone who needs to understand both mathematics and customer requirements. But I am not going at address that issue because I'm not interested in customers or marketing or management; I'm interested in computation.

And, frankly, it rankles that hardly anyone is able to talk about programming or computation without dragging commercialization or corporatism or capitalism or economics or politics into it. This, again, tends to obscure rather than clarify the issues. Certainly it is true that these things can be integrated with computing science as part of another field; but they are not a part of computing science itself, and I will oppose anyone who tries to co-opt the term for those purposes.

I am specifically using "programming" to refer to the aspects of this process which are applied mathematics.

I generally make a distinction between computer science, the general study of computation, and software development, the discipline of solving problems through programming (commercial problems or not).

They are both important, they are related, but they have different ends.

I can't avoid feeling, however, that unqualified "programming" belongs to the latter, more than in part because any large piece of software that has a user base, however theoretical its aims, tends to require some of the fuzzy techniques of software development along the way.

And, frankly, it rankles that hardly anyone is able to talk about programming or computation without dragging commercialization or corporatism or capitalism or economics or politics into it.

Consider the following:

A software developer is someone who, in order to make a living at what he loves, programming, agrees to put up with colleagues, customers and fuzzy requirements.

A computer scienitist is someone who, in order to make a living at what he loves, studying computation, agrees to put up with universities, students and publishing.

Of course, we can separate the activities from the professions in the abstract, but in both cases, the professions add a lot of complications to the activities.

"conflating programming with commercial software production" - yes, you're right, that's a fair point.

I think the problem should really be restated to take account of whether we are talking about programming solely at the "micro" level, in which case everything you say is true, or at the "macro" level inhabited by us commercial software developers in which case other factors also come into play.

The real ambiguity is in exactly what we mean by the word "programming".

I think the word "programming" is doomed to the same fate as "writing": a general term describing things that have little in common. A novelist, a journalist, and a mathematician all "write"; likewise, a weekend hacker, a DBA, and a shrinkwrap-software developer all "program". In both cases, there's a surface similarity, but what's actually going on is quite different.

...of course, is that we're still using languages/machine abstractions that allow such errors. :) Of course, that's not the whole story--improper requirements and poor development practice probably contribute quite a bit too.

But it's an interesting phenomenon of CS that the "safe" languages are often used only for application code, whereas the infrastructure and middleware is often written in C.

IMHO, the two biggest problems in software development are:

1. C won so decisively that its runtime environment became so pervasive that extremely intelligent professional programmers literally can't imagine anything else, to the point where they forget that C even has a runtime environment. This shows up in the "but even the Lisp Machine must have been running C or assembly language at the hardware level, right?" claims that I still hear when the subject comes up. Well, OK, yes, "assembly language" in the form of LAP... the more pernicious problem now is the grief that the C runtime assumption imposes when you want to write in an actual high-level language but take advantage of OS services. You're now in FFI-land. Yech.
2. Two-valued logic, with just "true" and "false" values. And no, I'm not suggesting SQL's "true," "false," or "NULL" as a replacement!

Just imagine how different computing would be if every machine shipped didn't assume the C memory model and C ABI, and if our first programming languages had supported probabilistic computing akin to IBAL.

WRT the first point, a link that might be of interest: Daniel Barlow picked me up for saying, in an advogato article on language popularity, for saying, about C++ that it does, as far as possible, respect the principle of runtimelessness, that is, the language does not force run-time overheads upon the programmer unless they are asked for.

WRT the second: I have no problems with 2-valued semantics, I only object to what Michael Dummett calls the presumption of the principle of bivlance on behalf of logics that admit 2-values semantics. To be more precise, just because Goedel's completeness theorem tells you that the required maximal consistent sets ought to exist, doesn't tell you that there is one that (i) actually exists, and (ii) would be a decent model for the logic.

The times, they are a-changing, check out House, where the Haskell runtime is the operating system.

Recent notable additions are the NE2000 driver and the TCP/IP stack, all in Haskell.

Now I just have to figure out to get QuickCheckM to work with the IO monad so I can get counterpane to hire me...

--Shae Erisson - ScannedInAvian.com

Strong Perl skills with the ability to quickly implement small to moderately complex scripts. Very strong Perl regular expression skills with expressions exceeding 1-2k length. Knowledge of available Perl modules sufficient to quickly achieve complex tasks with minimal effort. Equivalent Java programming experience a plus.

This from the counterpane careers section. 1K of regular expression! That way madness lies. And really it would be extremely easy to implement a little RE DSL that provided some abstraction mechanisms to tame this beast.

Regarding languages (natural ones, that is), I don't know that I would teach English compisition and Latin to CS students (as Mr. Holub suggests), but I might want them to take some philosophy of language (for issues of sense and reference, compositionality and meaninglessness, etc.) and, if possible, some mathematically-flavored semantics, e.g., the kinds of things covered in James McCawley's "Everything that Linguists Have Always Wanted to Know about Logic (but Were Ashamed to Ask)" (now with expanded coverage of lambda calculus in the second edition!).

Like I say, just for the record :) .

I took it out as soon as it was on the library shelves. Its a very fine read indeed, and I would recommend it to anyone. She departs with many expositions of the theorem by showing it as a consequence of the diagonal lemma. Of course, this takes much of the intellectual burden away from the exposition, but gives a wider audience a chance to appreciate the actual truth of the theorem, rather than imprecise postmodern adaptations.

Its funny, as when I mentioned that I was interested in studying logic to a professor of literary theory, the response was something along the lines of "oh, haven't you heard of... I think his name is Gödel, or something. Anyway, he proved that all of that is meaningless."

My two cents on the discussion: the non-CS courses that have impacted my CS work the most were Abstract Algebra and Set Theory. For instance, when I make abstractions in OOP, they tend to be more of a mathematical nature now, rather than anthropomorphisms. Abstract algebra can also be a good route for learning linear algebra, for those CS people that need it (see "Rings, Modules, and Linear Algebra" by Hartley and Hawkes).