Text this: Formal proofs concerning partial recursive functions.