Why learn applied formal methods?

  • Article

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,
https://www.paulgraham.com/avg.html

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