On theorem proving for program checking: historical perspective and recent developments