Linking the Meaning of Programs to What the Compiler Can Verify