I've written correctness proofs for C code, both as part of my university classes and after. Unless rust has some kind of de brujn criterion (and properly form

I've written correctness proofs for C code, both as part of my university classes and after. Unless rust has some kind of de brujn criterion (and properly formalising and bootstrapping it from a minimal core would be a step into that direction) the proof it produces is only as good as the entirety of the codebase. Correctness proofs are an inherently human thing, it's all about convincing your opponent of the proofs validity. One could of course build a language on inuitionistic math a a la coq, but that's neither practical nor realistic, so human checked proofs will have to do, and simplicity helps a lot with those. Edit: It feels like we're talking about subtly different definitions of correctness. I mainly care about correctness of specific program instances, whereas you are more concerned about the correctness of every instance expressable by the language.