Great article. I did want to add one thing that may or may not be relevant given this is targeted to people trying formal methods out. Just something I’ve consistently warned people about since it was common, stumbling block.
“This means that trying specifications, unlike trying new languages, does not carry a risk of technical debt or add any maintenance burden. You also don’t have to change the code to make writing specs possible. This all reduces the friction of experimenting with FM.”
This is true while formal methods don’t matter for the project. It can change if it becomes part of the workflow. In early and recent projects, they would have a copy of their English requirements, their formal specs, and code. The drawback that came with their benefits was having to keep these in sync. Sometimes folks got lazy. Other times, a change in one didn’t match the other due to abstract vs concrete types mismatch (eg numbers vs modular arithmetic). That increased demand for spec-to-code generation.
This might not matter if they exclusively use specs for throwaway prototypes. Keeping the specs around delivers biggest benefits. If they want those benefits, I advise to always warn that there’s some time they have to invest in keeping them sync’d. It’s like maintaining good, up-to-date docs.