Programming Language and Theorem Prover