Turns out that that boring stuff - type theory - they throw at you in uni, can be quite useful. Not only can it help with things like memory safety but also with speed. This is why for instance C++ std::sort() is faster than C qsort(), better type information available to the compiler allows it to make better optimizations. In rust the type system is king.
No, in Ada the type system is king. If type theory is the solution, then Ada and SPARK, Ada's restricted subset for extra safety, leave Rust in the dust.
