Program verification and semantics: The early work