My Authors
Read all threads
This is one of the most common questions about formal methods: how do I rigorously translate a spec to implementation, and how do I keep them in sync?

Short answer: you can't.

Long answer: you can, but it's incredibly difficult and rarely worth the effort.
There's two different kinds of "keep in sync": **synthesis**, where you generate code from a spec, and **refinement**, where you independently implement the spec and then show the implementation and the spec matches. These are the holy grails of formal methods research.
Synthesis is science fiction. There's some really cool research right now (such as comcom.csail.mit.edu/comcom/#welcome and github.com/UBC-NSS/pgo), but they're focused on narrow specs that are very close to code, and they translate to specific languages. Arbitrary synthesis? Not happening.
Consider the difficulty of doing machine translation between two languages with near-equal "power": write a program that takes a Python program and outputs an equivalent Haskell program. You'd consider that ludicrous. Now imagine trying to synthesize temporal hyperproperties.
(Note: synthesis is different from **extraction**, where you extract a program from a proven low-level spec. This is doable, but runs into similar problems as we'll see with refinement: it makes writing the spec vastly harder and eliminates a lot of the "expressivity" of specs.)
Refinement is a lot easier. You're not automatically generating an implementation, you're just showing an existing one matches the spec. This is doable, and there's plenty of tools for this! It's useful in a lot of industries and sees a lot of productive research.
The problem? Refinement is HARD. It is hard and expensive. You have to manually prove the correspondence. You need to be an expert in both the spec and the implementation and have deep mechanical sympathy with the tooling you're using to show refinement.
Some of this we can automate, but the more expressive you want your spec to be, the less we can automate. With specs you can handwave away things like "the process of retrieving and parsing the CSV", and now you have to prove all that implementation matches the handwave.
Again, it's not impossible. But it's often _infeasible_: it just costs too much time and money that's better spent doing other things. Which is why in the industry, we usually just assume there's no way to connect the spec and the code. It's just an economic reality.
Some people find this demoralizing. I find it reassuring. It means we're not selling snake oil. We're pitching an approach that has known, understood limitations. Formal Methods isn't the magic solution to all your problems, and we're okay with this! It makes it _real_.
But that probably doesn't reassure you. If you can't keep the code and spec in sync, why bother? Two answers to this:

1. Specs are more expressive in code, so they're a lot smaller. A thousand line change to the code might mean only a 1-line change to the spec.
2. You write a bunch of code and run into a very nasty bug in prod. Would you rather know the design is correct and it must be an error in implementing the design, or have no idea whether the problem is with the code or the fundamental design?
Ultimately, we write specifications because it works. It saves time and money. We'd save more time and money if we had easy synthesis and refinement, but we don't, and we're realistic about our expectations. And even then, it saves time and money. hillelwayne.com/post/business-…
If you want to learn more, I wrote a longer essay on the history, limitations, and developments in formal methods: hillelwayne.com/post/why-dont-…
I also teach people these tools as my business. This was a sales pitch, srry hillelwayne.com/consulting/

In the near future I have two slots remaining for a 1-day alloy workshop: eventbrite.com.au/e/software-mod…
Finally I got a newsletter where I rant about this and other stuff, like software history and empirical software engineering. Thanks for reading! buttondown.email/hillelwayne/
PS: I, uh, just realized I didn't answer the original question, which is "HOW do you translate the spec"? Code review! Formal methods doesn't mean you get to stop being an engineer, sorry. We still rely on our skill and expertise to reach the final code, FM just helps as a tool
See also this talk, where formal proofs are often (correctly) overruled for valid infrastructural reasons
PS PS: One underexplored but promising technique is to use the formal spec to synthesize/refine *tests*, not *implementation*. This sidesteps some of the difficulty issues here. Or to generate "ideas" for tests that are manually written by an expert.
Missing some Tweet in this thread? You can try to force a refresh.

Enjoying this thread?

Keep Current with Hillel

Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!

Twitter may remove this content at anytime, convert it as a PDF, save and print for later use!

Try unrolling a thread yourself!

how to unroll video

1) Follow Thread Reader App on Twitter so you can easily mention us!

2) Go to a Twitter thread (series of Tweets by the same owner) and mention us with a keyword "unroll" @threadreaderapp unroll

You can practice here first or read more on our help page!

Follow Us on Twitter!

Did Thread Reader help you today?

Support us! We are indie developers!


This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3.00/month or $30.00/year) and get exclusive features!

Become Premium

Too expensive? Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal Become our Patreon

Thank you for your support!