> at what level you could enforce/how far you could take the idea of "don't allow invalid states to be represented" to a programming language

Standard ML, Haskell, and Lisp, among other languages are pretty serious about invalid states. One should never be able to break the virtual machine and put it into an unknown state, unless intentionally mucking around with unsafe {} or its equivalent. Rust is often described as being at least partly in the ML family because of its approach to types and safety, which is very ML-ish.

Dependent typing like in Rocq goes even further, and makes it impossible to express invalid algorithms. Expressing practical programs in formal terms like that is rather hard though. It largely goes over my head, for sure.