Been a while since I took the intro CS course from Matthias at Rice (late 90s), but I do remember he was an eloquent teacher who really illuminated for me the idea that you could simplify the design of complex programs through formal techniques (as opposed to the cowboy coding I had picked up in high school). Whether or not I was always disciplined going forward, I've often felt the nudge to take a deep breath and think a bit more because of the image of Matthias speaking so emphatically about these things in my mind.
I'd like to see a HtDP/Racket attempt at Cleanroom to see what differences or similarities there would be. SPARK Ada and miniKanren, too. It's already closer to them with its algebraic style of specification of programs that use only a few primitives for easier analysis. Edit to add that what DonaldPShimoda describes is exactly what Cleanroom required with its "intended functions."
Had a look at the article you linked to, thanks for sharing.
I've done some work (in projects, not academia) on trying to create low-defect software - by informal methods, not formal verification, so the paper was interesting.
Matthew Flatt (at Utah, advisee of Matthias) teaches the same way. He emphasizes test-driven development and formal methods for designing a program that will work.
One of my favorite tricks I picked up was to write the header comment for a function before writing any of the code. Once you've written down what the function is meant to do, it's often almost trivial to actually implement. (This is especially helpful when first learning recursion, as I was when I took the class.)
