By reference? Yes.

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...

I wrote a small blog post about the idea:

https://www.spiria.com/en/blog/desktop-software/hypothetical...