As I am teaching Software Verification, I am leaning on an analogy that symbolic execution corresponds to expressions in a given programming language while Hoare logic corresponds to statements. It's vague but to the extent that your language has "pure" and "imperative" bits to it, symbolic execution and Hoare logic are frameworks for reasoning about them. But I've long felt that the theory beyond that level is poorly settled. The way I see it, most programs have structure at roughly four lev...
