> This is why formal specifications matter. note that "formal specifications" generally means "specification written in a formal language", very often in Hoare

> This is why formal specifications matter. note that "formal specifications" generally means "specification written in a formal language", very often in Hoare logic. Here's a paper that presents one possible way to formalize the building blocks for control flow (if and goto basically) in a very, very, very, very simple language: https://www.cse.psu.edu/~gxt29/papers/controllogic.pdf https://www.cse.psu.edu/~gxt29/papers/controllogic.pdf ; the core is Fig. 3. Let's be honest: maybe 0.00001% of anyone programming can understand this properly without spending 100 hours on learning the associated formal baggage. Doing something like this at the scale of "real" languages is unrealistic and useless: how many contributors GCC or LLVM would have if the requirement was to be able to parse Hoare logic fluently to transpose e.g. the C / C++ formal spec into code ?