> This kind of implementation is actually quite concerning, because it means you're punting through a language which is notorious for its heavy reliance on unde

> This kind of implementation is actually quite concerning, because it means you're punting through a language which is notorious for its heavy reliance on undefined behavior, and there is no way to opt out of undefined behavior in some cases. if it were a new project I'd agree, but if there's an existing C codebase, it already contains all these UBs and the goal of the rewrite is to grow a formally-verified critical core functionality in ATS that would still inline the rest of the project intact. This way the formally verified part of the project can grow naturally through small iterative steps without major disruptive changes to the tooling and supportive infrastructure. People who are familiar with C can acquire basic ATS patterns pretty quickly (within a month or so), and the same is applicable to those who are familiar with ML-family languages.