Earlier quoted context omitted.
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…
I like this idea too, but bear in mind that the world of SMT in general (Z3 not an exception) seems to have a lot of cosmetically-similar formulations some of which are trivial and some of which will take forever to solve. 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…
Re: Jonathan Blow on Rust
#51I wrote a paper on this a few years ago http://moskal.me/pdf/prtrig.pdf though indeed getting the quantifiers to verify is more art than science...