What is interesting is that the (core?) of OpenSSL was re-written in Coq according to the author. Then the natural question can that representation be used to generate C code from it and would that make a safer product.
From what I read the Coq specification itself wasn't complete or used to discover the vulnerability.
Would be great if the author shed some light here.
A C implementation seems inevitable, but an easy-to-link Rust implementation would be very nice to have.