Reading through your various replies to comments, it seems your argument boils down to the FFI issue, and I find that a little bizarre. Sure, ATS can inline lib

Reading through your various replies to comments, it seems your argument boils down to the FFI issue, and I find that a little bizarre. Sure, ATS can inline library calls due to the lack of an FFI, and maybe it has a cleaner interface to those libraries, but now you've introduced a completely different set of problems: now you have to tell the compiler how to prove your code. In my experience, learning the fundamental concepts behind theorem proving is a lot harder of a problem than writing an FFI interface to a library. In fact, that problem is so easily solved that there are tools that do 99% of the work for you. And sure, maybe rust will never be able to inline C code, but inlining function calls is such a trivially small performance gap that most applications would never know the difference. I'm not convinced that there are better alternatives for contributing to or incrementally rewriting an existing code base. FFI is for most purposes a trivial impediment compared to the alternatives.