The Principle of Type Inference

The principle is roughly the same. You can just imagine it as a good basis for a way to construct proofs by some definition of what you want to classify a proof as. Like let's say in our case, like what it means for a value to have a staring type and then how do I prove that? The steps by which you end up concluding that something has a particular type are exactly the same. This reminds me a little bit like the set theory and type theory in math kind of reminds me of like paradigms in programming,. And all of them are able to result in like a CPU executing instructions and doing stuff with memory.