My third relevant computer “experience:” When I enrolled at the University of Maryland in 1982, I had to sign up for a “weed-out” course as my introduction to the computer science department. The course CMSC 110P (the “P” was for Pascal, added that year to replace Fortran) introduced us to some wacky notion called A Calculus of Computer Programming. The esteemed Ben Schneiderman apparently had his hand in the “book” that backed the material, which in reality was a half-ream of paper rubberbanded together.
The course was all about how to create proofs of code, starting with individual operations and moving up to entire functions. It was a very tedious process. If I recall correctly, the course introduced its own proof language, one that bootstrapped itself. (I wish I still had the manuscript since I can’t remember what it looks like). Everyone in the class hated it. It drove me nuts initially, but it did make a big impression on me in terms of how difficult it was to code demonstrably correct functions. I remember spending half the semester on proving a few simple functions.
Wikipedia has some interesting pages about lambda calculus and functional programming languages. I never tried Haskell or ML. The notion of using functional languages to help in programming defect-free code sounds intriguing but also very tedious. Today I still recognize that creating correct code is a significant challenge. While it’s not the same thing, I view TDD as my way of demonstrating similar levels of control over what I produce.
