Lightweight Formal Methods: String Diagrams
On the Air team we recently started building a document generation and editing workflow focused around two goals: 1) reducing manual effort in generating air waybills, and 2) helping to clean up data entered into our system. This was necessary because air waybills were originally modeled in our codebase as a similar document — the ocean bill of lading — by engineers working off the best available information at the time.
This quickly became a problem during the architectural design phase. The flowcharts and call graphs of the old system were already complex, but overlaying the new components transformed the diagrams into something that resembled a modern art rendition of spaghetti and meatballs.
We needed something different. We needed formal methods.
Ultimately, “formal methods” is a scary way of saying that we took advantage of string diagrams. They are formal, in the sense that they have a well-defined mathematical meaning, and a method, in the sense that we used it. Above is a fairly straightforward example of the technique, describing how to prepare a lemon meringue pie. The lines coming in from the left represent input data, boxes represent systems acting on those inputs, and then lines exiting to the right represent output data. The representation allows us to hide complexity that’s not useful during the design phase of a system (e.g., how does one /actually/ produce meringue?), but also allows us to zoom in and draw in more detail where necessary — each box can be filled out with a smaller string diagram as long as all the inputs and outputs line up.
For a more concrete example, the string diagram for our Air Waybill project looks like this:
Hopefully, this is pretty straightforward. We take specific, labeled information from several subsystems — shipper & consignee from shipments, specific flight details generated from the route and flight info, etc — and funnel them through to the House Air Waybill system. Future systems (and the input information!) like the Master Air Waybill (MAWB) are represented via dashed lines.The colorful ‘Versioned Docs’ system was added during a design sync meeting between engineers where we were discussing downstream reporting requirements.
There’s a lot of complexity around exactly how the bill of lading is integrated with downstream systems, but using a string diagram allowed us to be confident that we don’t actually need to deal with that yet. We also don’t need to deal with where the systems on the left hand side get their information either, but if we did, it’s a matter of extending out the diagram with more strings to the left or drawing a box around this system and sketching out the upper level.
And, most importantly, the whole team can collaborate in on the design. In the string diagram above the colored segment was added in a quick architecture design sync during a discussion centered around reporting requirements. The flexibility of the drawing gives us the power to make these changes live, but it’s the mathematical formalism that gives the whole team common ground to interpret exactly what those changes mean.
It’s the regularity and predictability of the formal model is what allows us to avoid becoming tangled up in flowchart spaghetti.
