I would quibble with what keywords they are using in a few places, but it sure seems interesting. My work is less interested in making sure the program is correct, because I'm trying to do knowledge representation of a thing that might not be. Being able to still run queries when part of the code doesn't make any sense - because the law it models doesn't make any sense - is part of what I need. So verification is sort of worthless to me. The "we don't know, we might convert it to first order logic and throw z3 at it or something" approach seems a bit... sketchy. That doesn't give me a lot of hope that it delivers on the promises of validation. But co-opting a bunch of game developers into testing your language by deploying it as the scripting language for your huge hit game is a unique play.