My work on formally specifying web page layouts often has people asking how web page layouts—which after all are esthetic as much as they are functional—could possibly follow a specification in pure logic. I understand the confusion: we too often think of a program as having an end-to-end specification, and that the point of verification is to allow us to treat the program as a black box, secure in the understanding that it follows the spec. That is an unusual special case. Most programs ...
