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…
I really like this idea. I’ve been messing around with the z3 theorem prover, and while I don’t think there’s an easy way to integrate it to do compile-time checks, I made a little wrapper class that lets you add assertions which are checked for satisfiability at the end of a function’s scope. But it’s all at runtime, so it’s more like a more advanced assert() than anything like Jai or Rust has. I think SMT solvers a…
The honeymoon with SMT is often brief. You've gotten through the whole 'hooray, now I can nuke Sudoko and those "Mr Brown lives on the same street as the baker, who has a white house" problems' and surely all the world's problems will fall to my awesome new abilities. You then put some basic quantifier problems into Z3 or whatever and watch the prompt go away, apparently permanently.
I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research.