YAY! That's extremely good news. Thanks a lot!
I particularly love to see _full_ H3 - incl. 'invariant'. 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.
Last but not least, having some capabilities and/or interface to formal
analysis would (IMO) pretty much close the gap between Nim and Ada+Spark plus
it would open the door to (step by step) have Nim's stdlib and some major Nim
libs fully verified. That plus the fact that Nim, while (still) lacking some of
Ada's strengths, also has some strengths that Ada does not have (and is
extremely unlikely to ever get) could make Nim _preferrable_ over Ada.
I'm really enchanted by the news. Thanks so much @Araq and Nim team! [pls.
imagine a "heart" icon here which to make/insert I'm too clueless]
