I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works.

In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS heap, and then we have system objects involved in basic I/O that aren't necessarily tied to a particular JS isolate and are not garbage collected, but are often tied to specific OS threads. JS objects and system objects are allowed to own instances of each other, but the ownership must be handled in a special way. E.g., when a system object holds a reference to a JS object, the destructor must ensure the JS isolate lock is held before releasing that reference. Conversely when a JS object holds ownership of a system object, and the JS object is garbage collected, we need to queue the system object's destructor to run in the thread where it was created.

Conceptually, it ought to be easy to write rules where each type is declared as being a system type or a JS type, and then the compiler could trivially enforce that the correct sort of references are used between them. But, the problem is very specific to our codebase, so it would make no sense to bake into the language.

I think the next big thing for C++ should be adding ways to define custom code-checking rules like this. It would allow C++ to become a safe language and would fit perfectly with C++'s culture of being ridiculously overcomplicated. ;)