Comment by hansvm

This sort of idea is why I sketched out pdv [0] in Zig. Even extremely simple type systems can handle arbitrary invariants when you are allowed to compute with those invariants at compile time.

[0] https://github.com/hmusgrave/pdv