Sure, it’s important for a library to have C source code for portability. That doesn’t exclude implementing the code in another language (such as F*/FStar or Da

Sure, it’s important for a library to have C source code for portability. That doesn’t exclude implementing the code in another language (such as F*/FStar or Dafny) that has stronger out-of-the-box safety guarantees, then compiling it to portable C source code for distribution.