Dijkstra: On the cruelty of really teaching computer science (1988) [pdf]

As someone who focused on proof based mathematics in collage and is largely a self taught programer I think this proposal has merit. Begin forced to confront abstraction and formalism without any crutches as a freshman in college changed and expanded the way I thought. Learning to write down a correct proof without an external way of verifying it is an experience everyone should have.

However I think this needs to be coupled with an introduction to the concrete at a younger age. In mathematics we teach arithmetic to young children then step up the ladder of abstraction to high school algebra, simple proofs and linear algebra before eventually exposing them to abstract algebra (ie group theory etc). Teaching abstract algebra first would make theoretical sense but the mind tends to need to know at least one example of something before it accepts the abstraction.

I imagine a playful introduction to programing for young children coupled with a strong course in formalism for young adults could produce some great programers. Though, as with the proof based math series I took, I'm sure there would also be loads of freshman drop outs/transfers to more applied courses.

I also agree with others that insight rarely comes from pure formalism. The point of learning these things is to expand the way your mind works allowing you to think about abstract objects and allowing you to verify insight when it does come.

For me Charlie Parker sums up the necessity of a formal education even if it is not explicitly used in practice:

"Master your instrument, master the music & then forget all that & just play."

>Do you understand the difference between "formalizing all reasoning" and just formalizing something?

Thanks for the condescending tone. But, you need to start somewhere. Be realistic.

Are you sitting and complaining that since physicists don't have a theory of everything already they should stop their work? Are you sitting and complaining that since we have not yet gone to Mars, NASA should be shut down? Are you also complaining that since we don't understand the genome fully, we should stop computational biology?

We start with approximations and we need to start small. Like in any science. Claiming reasoning is unformalizable is appealing to superstition and folk science.

And I was responding to the point that formalization has zero real world impact. That is patently false and intentional middle-brow FUD. This FUD can cause real harm to real people (not just people who study formal methods.)

You still have not responded to my example of formal methods being used in the real world with real impact.

> just like not that many new theorems in mathematics, outside of mathematical logic, were discovered using the tools of mathematical logic.

That is plain FUD right there.

> What I am saying in the comment is that I do not believe many people benefit that much from a formal approach to program development

A lot of systems would benefit from formal (or more formal) methods. I worked in aviation software, formal methods would have saved us so much trouble, especially since the code size is often relatively small (10k-200k LOC) and because we're dealing with other systems the IO spec was reasonably complete. Sure there'd be issues, but feature creep was not one of them (except on one project). Feature creep makes formalisms difficult, but only when you're looking at whole program formalisms. So certainly safety critical systems benefit.

What else might? How about medical systems (see Therac-25 for faulty UI leading to deaths). Network code, especially fundamentals like routers, switches and core services like DNS that so much depends on. Cryptographic and other security systems. Compilers, obviously, similar to network code they're too ubiquitous to be left to error prone ad hoc approaches. Anything handling money. Anything handling privacy (ensuring HIPAA and whatever European privacy rights). Software handling production automation or managing warehouses/inventory, failures there mean lost production time, wasted inventory, lots of money and productivity gains to be had by having software that works.

If you accept formal methods on the small scale (essentially the promise of functional programming a la Haskell and the ML family), you can be confident in composing large systems out of smaller, formally verified systems.

I had a student of EDW as my Programming Languages instructor. Someone asked my prof, "How do you debug?" His response, "I don't. I prove that the code is correct before I type anything."