I assume you're asking why the underlying crypto still needs to be written in asm. There are two primary reasons:
1. Performance
2. Defense against side channel attacks (e.g. constant time operations)
1. Performance
2. Defense against side channel attacks (e.g. constant time operations)
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.