Embed Notice

@penguin42 @edavies @thephd
The concept you’re reaching toward here is “dependent types:” https://en.wikipedia.org/wiki/Dependent_type

In short: types can carry logical constraints, e.g. not just “integer” but “integer in a range;” not just “list of T,” but “list of T whose elements are in sorted order.” You can statically verify types like that if and only if you can show the compiler how to •prove• those logical conditions are met — and so…