I very much hope that some next big crypto / security library will be designed and tested in some rigorous language like Haskell, its key parts proven correct with something like Coq, and then an efficient and portable implementation code generated automatically.

A C implementation seems inevitable, but an easy-to-link Rust implementation would be very nice to have.