High-assurance systems of the 70's-80's used formal specification in languages like Z and VDM to increase correctness of software. These were often hard to use

High-assurance systems of the 70's-80's used formal specification in languages like Z and VDM to increase correctness of software. These were often hard to use for a lot of people involved. The ASM's did similar stuff in a way that's easy for programmers and even non-programmers to understand. Lots of tooling got built for various stages of ASM development. These and similar things like B method (esp Atlier-B) were used in industry to produce highly-robust software proven correct from requirements to design to accurate models of code. Most verification uses Coq, Isabelle/HOL, etc these days. Closest thing to this with adoption is TLA+. People using that or frustrated with the difficulty of semantic methods definitely should look into ASM's. Survey of many uses of the method: https://pdfs.semanticscholar.org/81aa/8726219c4145ff6b8932837203d07b34b51e.pdf https://pdfs.semanticscholar.org/81aa/8726219c4145ff6b893283... Use in verified compilation is particularly interesting. The components are so small vs what I see in semantic methods. Here's the best one that I'm aware of: http://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf http://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf