But the idea of a verified type can be extended by using the verified modifier on your own type. For example, you could have a verified matrix type, where the matrix is guaranteed to be valid, non-degenerate. You can apply it to:
- matrix
- vector
- input data of any sort
And if teh compiler allowed the programmer to declare their own type modifier, the world is your oyster: you could for example tag that a matrix is a world matrix while another a local matrix and provide a function that converts from one to the other...
But the idea of a verified type can be extended by using the verified modifier on your own type. For example, you could have a verified matrix type, where the matrix is guaranteed to be valid, non-degenerate. You can apply it to:
And if teh compiler allowed the programmer to declare their own type modifier, the world is your oyster: you could for example tag that a matrix is a world matrix while another a local matrix and provide a function that converts from one to the other...I wrote a small blog post about the idea:
https://www.spiria.com/en/blog/desktop-software/hypothetical...