> Are there also plans to provide quantors ('forall', 'exists' (plus
> negation))? Even hotter: Are there plans to provide a compile time interface
> to Z3? I'm asking because that would be the "sweet spot" in terms of the
> least work for the Nim team while providing full formal capabilities for
> those (probably rather few) Nim developers who need full formal verification,
> some kind of transfer to/from model checkers, etc.
Quantors are coming and so is negation. We also attach pre- and postconditions
to proc _types_ so that `method` and function pointers work. And the analysis
is modular, it doesn't look inside proc bodies. We use the Z3 nimble package to
interface with it, there is no "compile time interface to Z3" though as I have
no idea what that would look like. We strive to map large portions of Nim to Z3
though including floating point and unsigned math.
