ezyang’s blog

the arc of software bends towards understanding

Abstraction without a concrete concept

Hoare logic, despite its mathematical sounding name, is actually a quite practical way of reasoning about programs that most software engineers subconsciously employ in the form of preconditions and postconditions. It explicitly axiomatizes things that are common sense to a programmer: for example, a NOP should not change any conditions, or if a line of […]

  • October 6, 2010