r/formalmethods

In the early 2000s, verification tools (like Boogie) adopted an operational "desugaring" approach to handle unstructured control flow, favoring speed and SMT solver compatibility. However, by elevating assume to a first-class primitive, these tools arguably commit a category error. They shift verification from axiomatic deduction to operational state manipulation, effectively allowing "miracles" (violations of Dijkstra’s Law of the Excluded Miracle) to mask bugs as vacuous truths. This analysis explores why Leino's operational approach, while pragmatic, departs from the theoretical rigor of Chen's axiomatic fixed-point framework.