Comment by ashton314

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?