Typed assembly is a thing - it’s mainly to ensure the compiler itself is correct, but it does give stronger guarantees. I think Frank Pfenning at CMU has writte

Typed assembly is a thing - it’s mainly to ensure the compiler itself is correct, but it does give stronger guarantees. I think Frank Pfenning at CMU has written a language that’s dependently typed all the way down - so it’s IR and assembly are both dependently typed.