These are tools. How well they work largely depends on the discipline and processes followed by the development team using them. If the concern is that raw poin

These are tools. How well they work largely depends on the discipline and processes followed by the development team using them. If the concern is that raw pointers can be extracted from controlled pointers, then the development team needs to check for this. No tool is perfect, but tools like these can be used effectively to reduce attack surfaces and improve safety. Even languages like Rust make memory safety optional. One can drop into an unsafe block and perform all sorts of abominable things. Such escape hatches are necessary to color outside of the lines when one must do system software development or optimize software beyond what the compiler can do on its own. At some point, the developer must be trusted to learn the tool or to use discretion when considering something like unsafe. In both cases, a development team can peer review these choices. What makes me interested in tools like Cake and similar tools is that these bring us closer to being able to use proof assistants to build up reasoning about the times when we must color outside of the lines. Whether C, C++, or Rust, being able to import code into a proof assistant or extract efficient code from a proof assistant can further assist us when our use cases exceed what is possible with the safety features in our language or tooling.