Formal Methods: Removing Industrial Adoption Barriers

Recently I had an opportunity to participate in the inaugural FormaliSE workshop. It had some interesting papers, but here I'll focus on the round-table discussion. Basically the problem is, research guys are in pain because code shops don't use their results. Among all the research guys, the formal methods (FM) guys are in most pain because formalisms are "eewwww," according to an average programmer Joe.

Despite quite a few local successes of formal methods, the "eewwww" perception is seen as a great challenge for the community. The discussion concentrated on overcoming the barriers to FM adoption in industry. Two major topics were on the table: software engineering (SE) education and lightweight formal methods. Below is a summary for the discussion:

• Software engineering education. 
• How similar does it have to be to the classic engineering education (mechanical, electrical, ...)? One extreme opinion was "software engineers should know basics of mechanical/... engineering" (rationale: otherwise often l) ad . The other extreme was that software engineering is a thing in itself, and even computer science should scrutinized for relevance to SE. However, most participants accepted that computer science provides most of the scientific base for SE. All this kinda relates back to the discussion of software engineering as engineering.
• Software engineering education should be smart about building appreciation for FM. We agreed that it's pointless to kick in Hoare logic before showing the fun of writing code. The fun part of FM is similar to that of code: formal methods allow to achieve some interesting result (e.g., find bugs). Therefore, assignments should have this useful result as a final deliverable, not some loop invariant that doesn't have much value on its own. Such assignments should build appreciation for FM early in the education and not let students emotionally reject formality in their further practice.
• Education isn't confined to colleges. For example, sometimes there's a necessity to educate government employees about a particular FM under stringent time constraints. This challenge hasn't been addressed much so far.
  
• Lightweight formal methods. 
• What does lightweight mean anyway? It is being used very informally. After some brainstorming we came up with three aspects/dimensions of FM "weight":
• Process: what part of the process do FM apply to? Is it used to specify requirements or generate tests?
• Product: what part of the product are FM applied to? Is it only the OS process scheduler or the end-user GUI?
• People: who is exposed to formality? Is it used to negotiate outsourcing between companies or hidden inside a clone finding tool?
• Being rigorous, but not formal may be a solution for contexts where FM fail. For instance, one can be more controlled/cautious about iterations (because they can introduce implicit faults) and use standards and process frameworks as a replacement for formal models.
• Heavyweight formal methods does not necessarily mean clumsy, inappropriate, useless, or unusable formal methods.

This was a summary of the discussion at FormaliSE. If you have any comments or questions, you're welcome to send me an email. Related reading:

• Seven Myths of Formal Methods -- an old paper busting some myths, which later outgrew the dilemma of myth vs. reality.
• Software Mythbusters Explore Formal Methods -- the CMU ISR people take another look at the "myths" two decades later.
• Formal Methods: Theory and Practice -- an overview of state-of-the-art in formal methods research and industry by some of the FormaliSE workshop organizers.
• Really Rethinking Formal Methods -- Dave Parnas on some popular opinions about formal methods.