Earlier quoted context omitted.
Is a "bound-checking memory-safe C compiler" even possible in the general case without implementing a new Rust-like language?
Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions. If done in a system like Coq or Isabelle, the proof obligations become a parallel markup to C that is used in conjunction with the source code to enforce policies. Bounds checking is one policy -- and a relatively easy one to implement at that -- and other po…
https://news.ycombinator.com/item?id=12407156
Difference between memory safety and full, formal verification of correctness. You're describing the latter. Definitely check out Myreen et al's CakeML work, COGENT at NICTA, and AutoCorres/Simpl used in seL4. They might have stuff to speed up your own tool development. I wish you great luck on your project. :)