That’s an interesting notion (although it underestimates the effort, I think). Honestly, having machinery to write down contract semantics in a fashion amenable to automated proofs (meaning, does it type-check?) is massively promising; and I’m a dyed-in-the-wool C hacker. I would hope that the public exposure of this bad behaviour causes a few moments of self-reflection.

I suspect that attempting to chase a moving target of describing C apis with rust is just an avenue for burnout, unless there really is a mechanism for getting fixes back in the other direction, and professional respect flowing in both directions. That would be a massive shame, and an incredible missed opportunity.