Has anyone in this space considered adding type annotations to assembly?
It’s totally possible and it’s a thing compilers for memory safe languages sometimes have to do internally.
It wouldn’t take a lot of language engineering to make it nice. You’d end up being able to take that asm code more or less as is and annotate it with just a type proof so that Rust/Go/Fil-C can call into that shit without worrying about it blowing up your rules.