Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, b

Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side. Now allow arbitrary programs to be types. We'll call these type programs. Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing. For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself. Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis. In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true. You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here. I find the whole thing fascinating myself, but haven't gone too deeply into it. (BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)