This is similar to program development using the B method, which is used for some safety-critical systems: https://en.wikipedia.org/wiki/B-Method https://en.wik

This is similar to program development using the B method, which is used for some safety-critical systems: https://en.wikipedia.org/wiki/B-Method https://en.wikipedia.org/wiki/B-Method There the idea is also to start from a general specification and an abstract program (not executable) that is refined stepwise into a final, executable program. At each stage you prove formally (using automated provers and a proof assistant) that the current program is indeed a refinement of the previous, more abstract one. From what I can tell, this would be a good way to develop many things, though the B method itself is hampered by terrible notation and a lack of availability of good toolchains.