I don’t really understand your point there. Sound type systems are equivalent to proof systems. You can use them to design data structures where their mere ev

I don’t really understand your point there. Sound type systems are equivalent to proof systems. You can use them to design data structures where their mere eventual existence guarantee the coherence and validity of your program’s state. The basic example is “Fin n” that carries at compile time the proof that you made the necessary bounds checks at runtime or by construction that you never exceeded some bound. Some languages allow you to build entire type level state machines! (eg. to represent these transactions and transitions)