The whole point of strongly statically typed languages is that the proofs are performed at compile time. Statically typed programs shouldn't change behaviour af

The whole point of strongly statically typed languages is that the proofs are performed at compile time. Statically typed programs shouldn't change behaviour after type erasure. Languages with strong enough type systems can statically guarantee that data is structured correctly at runtime. Stronger structural requirements require stronger type systems. Algebraic data types are sufficient for many common static structuring guarantees.