Reflections on Software Engineering

My view on formal methods is somewhat... nuanced.  In spite of this I'll go ahead and start with a ridiculously strong and outrageous assertion that I can use as a toe hold for further discussion:  Formal specifications do not have a place in agile software development.  Don't get me wrong. As a software engineer I like the idea of formal specifications very much.  They are precise.  They are unambiguous.  They are... engineering-y.  But as a post-modernist software engineer I also think formal specifications are kind of a dumb idea . They are tedious. They are cryptic. They are... anti-human. For decades software engineers seem to have put formal specifications on a pedestal as if they were the Michelangelo's David of requirements.   But while Michelangelo's sculpture of David manages to perfectly capture the essence of humanity in marble, even the most elegant formal specifications fail to fully capture the perfect essence of desired function...

Almost a full year ago, I concluded that formal methods simply aren’t worth the effort : For almost every project in the world, I think formal methods should be generally avoided. Given the option of spending money and time on mathematicians or extremely smart coders I would chose the latter. With smart coders, code inspection is a fun and effective defect filtering option. And let’s face it. Why would you have your amazing coders do something other than write amazing code? But what if formal methods didn’t have to be so...formal? While traditional formal methods such as Z might be a little difficult to pick up if your predicate logic is rusty, applying formalisms that are close to the code doesn’t seem that outrageous in perspective. Design-by-contract language extensions such as Spec# for C# or Plural for Java have been stealthily making their way into IDEs for years now without anyone really knowing the wiser, without anyone really thinking about these tools as be...

Are formal methods in software engineering really all they are cracked up to be? First, let me clarify what I mean by formal methods.  Formal methods use mathematical representations of software to formally prove that the software behaves as expected.  Most formal methods use predicate logic and set theory along with other mathematical notations to describe software in a formal specification.  Examples include Z (pronounced zed) , state machines (such as the finite state process algebra FSP), Petri Nets , the use of pre and post conditions, and the Object Constraint Language used in conjunction with class diagrams in UML.  Most formal methods have some kind of automated proof capability be it by brute force or through the use of more sophisticated theorem proving programs. Let's take a quick look at Z which is probably the most widely available formal specification method in terms of books, online documentation, and automated theorem provers.  Here’s a simp...