Hmmm, I can try to address your questions. 1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals. 2) Gene

Hmmm, I can try to address your questions. 1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals. 2) Generally the programs that are proofs you would want to be pure, but it wouldn't be strictly necessary. The impurity would have to be handled by the type system though, so explicit effects not side-effects. Also, note that even though you want the programs-that-are-proofs to be pure, that doesn't mean you can't prove things about programs that are impure - that is, you have a pure-program that has a type, and that type is a proposition about a different impure program. That is, I can create a pure program that is a proof about my impure program. EDIT: I think something that is a sticking point for a lot of people is looking for a program that is useful by itself that is also the proof of something useful. This is possible, but a bit rare-er - oftentimes you have useful programs with trivial types, or useful programs-that-are-proofs that you don't actually care to run. These are still super useful though! It is possible to have ones that are both - decidability of things is what comes to mind. You could write a program that determines if two naturals are equal - that's a useful program, albeit one of the simplest - and that program also serves as a proof that two naturals are either equal or not - a kind of particular instantiation of the law of excluded middle. One style of programming with dependent types always returns a proof along with the returned value, which might be kind-of what you're looking for. (Think of a regular expression engine that along with the yes/no does this string match this regular expression, returns a proof that the string does or doesn't match, demonstrating its own correctness)