I’m just about finished with the coursework portion for my MSE degree and figured my last quarter should have some fun classes instead of the “usual” ones. I’m taking a course called Applied Formal Methods. It’s all about writing specs using a formal notation, refining them until we get to a “program” and proving, along the way, that the program will be correct out of the box. There’s a ton of theory in this class, loads of unusual notation, not a small amount of math, and plenty of theorem proving.

So far we’ve been through basics proofs of if..then..else, while..loops, loop breaks, and for..loops. The question has come up several times in class and over a private email thread about how this course can a) be useful, b) be applied, and c) make it into the “real world”.

I've been thinking about this class for the last few weeks trying to come up with an answer to that question about how this stuff helps us design better programs. I think I've arrived at an answer only to realize that the answer was sitting right in front of me the whole time.

But first, a little background information to set the stage. Many of us took an Introduction to Programming or Principles of Programming Languages class some time as an undergraduate. There's a good chance that the tactics which you learned in that class never appeared to have any relevance to the rest of your undergrad work. [Insert any junior high student comment about how you’ll never use calculus or geometry in real life so there’s no reason to learn that either.] In fact, you might have thought at the time that none of what you were learning would ever be useful once you started designing or writing software.

Let's look at those topics for just a minute and see if they've be applicable to your career.

  • Abstraction building using procedures: expressions, the environment, scope, procedure application, black-box abstractions, recursion, growth and cost, procedures as data
  • Abstraction building using data: sequences, structures, sets, encoding, optimizations
  • Modularity, scope, state: variable scoping, assignment, volatile data, simulators, data structures, streams and infinite data structures
  • Abstraction: language evaluators, data as programs, programs as data, lambdas, closures, interpretation order, and programming models (logic, functional, imperative, declarative, applicative)
  • Machine architectures: register machines, routines, stack frames, allocators, garbage collection, tail recursion optimizations

So, given all that theory, what did we take away from it? The simple answer is that, although we might not feel we use these skills every day, we do use them. We use them without knowing that we use them, and they make us better designers and programmers. Learning that theory, even though we don't write a read-eval-print loop [see the Wizard Book if you don’t know what this is] every day, we know that it's the underlying technology on which interpreters, scripting languages, and debuggers are built. Although we don't implement red-black trees ourselves we know their performance characteristics and how they're implemented which allows us to make informed decisions about which data structures are best for a given application.

I did my undergraduate work long enough ago that we used LISP as the design and implementation language. I always wondered why I'd want to know LISP. Everything I'd seen up to that point had been BASIC, Pascal, C, Algol, COBOL, FORTRAN, or some other block-structured procedural language. I couldn't get my head around how LISP was going to help me write better C programs. Turns out I wasn't paying enough attention at the time and didn't realize that the concepts being taught are universal. They apply to every language, every program, every situation.

Formal methods are in the same boat. You may not directly apply the notations. You may not “prove” that a given algorithm meets a given requirement. You'll probably never find yourself doing formal refinement of a specification. But, you will start to think differently about how you write programs. You'll subtly change the way you think about requirements. You won't ask the customer to rewrite the requirements using CSP or Z or any of the other formal notations. But, when a customer asks you to implement a given requirement you'll stop for a minute and ask yourself if that requirement is strong enough to be implemented. Then you'll work with the customer to refine the specification until you both agree that it can be implemented, it can be tested, and it meets the customer's needs.

This isn't about learning a new technique for writing programs. It's about changing how your brain works when you start designing algorithms. Just like LISP teaches us how to rethink program constructs, formal methods teaches us how to rethink coding constructs. This is about adding two things to your toolbox: new tools and the skills to use them. (A few other useful tools are LISP-like languages, like Scheme, and functional languages like Haskell. I spent Winter break last year teaching my Haskell because I wanted to add something new to the toolbox.)

I'm waiting for the “formal methods” versions of the following papers. When that happens, formal methods will be the thing to learn. Again, not because we want to directly apply the “languages”, but because the concepts make us better.

Beating the Averages, Paul Graham, http://www.paulgraham.com/avg.html

How to Become a Hacker, Eric Raymond, http://www.catb.org/~esr/faqs/hacker-howto.html