A big part of the problem is trying to do this with C in the first place. The explicit memory operations create an extreme complexity in reasoning about a prog

A big part of the problem is trying to do this with C in the first place. The explicit memory operations create an extreme complexity in reasoning about a program exhaustively, not far from analyzing generic binary code. C is so permissive to be overkill for a lot of applications. Would this be more tractable with safer programming languages that avoid "wild" pointers, such as Rust? Or maybe by extending the C syntax so that the programmer can give hints to the compiler what he means, instead of what he has written so that the compiler can detect mismatches? BTW props on Frama-C, it's incredible what you guys are doing.