Comment by almostgotcaught
2 years ago
> "this register ranges from 0 to 4"
that's not a type system, that's an ILP. and we already have that in many compilers (bindings to ILP solvers).
> Maybe the ISA can now do something clever to further optimize my program.
this is a malformed sentence - the ISA is fixed and isn't making any gametime decisions about your code (modulo branch prediction/cache-fretching). it's all in the compiler and like i said we already have this in many many compilers and it's surfaced in various ways (eg trip count on loops).
Those who say it cannot be done should not interrupt someone doing it.
https://www.cs.cmu.edu/~rwh/papers/dtal/OGI-CSE-99-008.pdf
It's not perfect, but dependently typed assembly languages isn't something I just made up. Maybe there's a mismatch between the terms we're using?