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

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 https://github.com/hmusgrave/pdv