Proofs as usual written are informal summaries, but they are supposed (in today's age) to be linked to a very rigorous series of steps more precise than a Haske

Proofs as usual written are informal summaries, but they are supposed (in today's age) to be linked to a very rigorous series of steps more precise than a Haskell program. Actually, it's very similar to the execution of a Turing Machine (there are formal connections): * There is a finite set of logical rules. For example, one rule is that if A => B and B => C are true, then A => C is true. * We start with a finite set of given facts. * At each step, we state a new fact and note it is true by combining previous facts with a rule. * At the end, we have the claim we started with. Example: prove 14 is an even number. 1. If a number equals two times an integer, it is even (given fact). 2. 7 is an integer (given fact). 3. 14 = 2 times 7 (laws of multiplication). 4. 14 = 2 times an integer (combining (2) and (3)). 5. 14 is even (combining (1) and (4)). At a more complex level, e.g. proofs by induction are often no more than programs with for loops.