Types are propositions/theorems in some logic that’s paired with your language and values are proofs. I.e. a valid value X of type T is a proof that T is decidable and “true”.

Computation is merely simplifying a proof.

Depending on a set of typing rules it is sometimes possible to produce different “correct by construction” values that wouldn’t fuck you up. That’s decidability.

The fancier your language is, the easier it is to present a value that’s undecidable, uncomputable or otherwise FUBARd.

Propositions can be insidious when you try to convert between formal and informal intent. Consider what the stupidest value can satisfy your type while not doing any of the intended work (e.g. always returning empty list for “sort” function).

You need more fancier types to pin down exact details like “no, an empty list wouldn’t fly, do the actual sorting, you ass”.

Type inference is an epic win for programming. The fancier the types, the more difficult is inference.

Value inference (AKA proof search) is possible sometimes and is magic.

Those are basically the same with dependent typing. And it has its costs.

As they say, “a good type has half the value”. This cuts both ways.