Maybe not trippy, but a simple set of examples are existence theorems, i.e. "Given these objects, X exists." An example are fixed point theorems. Theorem: For

Maybe not trippy, but a simple set of examples are existence theorems, i.e. "Given these objects, X exists." An example are fixed point theorems. Theorem: For any function g from a convex, compact set to itself, there exists a fixed point of g. program f: g --> x where g is a function from a convex, compact set C to itself, and x satisfies g(x) = x. If you can write the program and it is correct for all such g, that is a proof that such a g always has a fixed point (in particular, you output one). Note the "type" of g is "function from convex, compact set to itself" and the "type" of x is "fixed point of g".