Hyperbolic

At Quanta today a nice article written for the masses tells about formal methods.

Many of us believe that such methods are what we need in the long run, not just for security but quality in general. We can’t get much solace from a program which defies malicious use if it also fails users with benevolent needs. And it turns out that the issues of security (itself a big definition) go hand-in-hand with the business of getting your functionality right.

Please understand a particular challenge called out in that article. It talks about hardening just some critical points (for security), and the reality is: designing with mixed levels of formalisms is incredibly hard. You would not presume a house is secure for having done a really good job on properties of the deadbolt lock if your door was not correctly fastened to the hinge side; you sort of need to know things about both, not just a lot about one side.

Other analogies apply. If you take a glass of pure spring water and drop in a bit of sewer water, you end up with sewer water; if you take a glass of sewer water and mix in pure spring water, then you still have sewer water. The suggestion is you’re no better off than the poorest piece of your system, and moreover systems are often not built from discrete blocks so much as code blends. Just pouring in some quality ingredients doesn’t make the rest palatable. You usually only know something strong about a program’s value once you see it in context.

Students in our program should reasonably ask what our department offers in the way of formal methods, whether just for security or for quality overall. Today the answer is “not much”, but years ago all students starting in our introductory programming sequence learned our crafts using formal methods (functional notations and some specification frameworks pioneered by a fellow named Harlan Mills.) The canonical ‘old guy’ observation is that we consistently graduated some of the best programmers of the era, which we attribute to the fact that they all learned fine code design in a framework that rewarded structures about which someone could reason. You had to take the time to make it clean and simple so you could meet the spec and move on. The debug-by-friction habits we see students picking up in our Java sequence (and often never shaking) would not get you far. As it turns out, and judging by what we see in learning outcomes assessments, those hack-and-slash techniques aren’t getting students very far today either.

What happened? The long-standing internecine warfare between field committees in our CS department left formal methods a thing of the past; software engineering lost. Today’s leadership has pretty much put a nail in the coffin of the robust software quality perspective which helped put our department on the map. This is true in our curriculum, and to a great extent even in our research, wherein resources and policies support the pet programs of select faculty doing other things.

And what a shame. The linked article makes clear the formal methods of that era grew and are blooming today, in ways we might never have dreamed but had certainly hoped. It is a space in which Maryland might have led. Our courses would certainly not be using tools from a couple decades ago – after all, our insights would improve over time as did everyone else’s – but we’d at least be in the game and talking authoritatively about the big picture of quality. Our campus leaders instead have just what they engineered: a department that, lacking its own vision, whores after dollars in a cybersecurity market built by others instead of setting the industry’s standard for quality (of which security is one piece).