[kobebrookskC3]

> there are products that offer memory-safety proofs for C

what does the c checked by this tool look like? for an example like https://play.rust-lang.org/?version=stable&mode=debug&editio... , does the tool accept the assignment with f and reject the assignment with g?

[pron]

That particular code is shaped by Rust's specific scoping an lifetime rules, but generally - yes (provided you offer annotations for things the tool can't infer). Some changes to the code may be needed to make things easier, but it's still a lot cheaper than a rewrite in a different language.

[kobebrookskC3]

in this example, aren't the scoping rules for c pretty much the same?

what do the annotations for the tool look like? is the analysis local, in that it doesn't look into the bodies of other functions? if it is, surely you would have to have lifetimes and be generic over them.

how much c code satisfies the tool? if there's hardly any c satisfying the tool, there might actually be a larger ecosystem of rust code to use.