Formal specification means building up this specification from theory, and building proofs along the way. Of course, there can always be errors in specificatio

Formal specification means building up this specification from theory, and building proofs along the way. Of course, there can always be errors in specification, but this is supposed to be the first place we implement SAT solvers or proof assistants. During Dijkstra's time, such technologies were not yet available as they are now. There is work to be done until this is all practical and the overhead to do this is within the current overhead of software engineering, but we are quickly reaching that point in time.