>>1073429I once specified custom invariants for arbitrary AST nodes that are used by a built-in semantic reasoner to prove programmer-specified assertions, which can be used to verify consistency (the way a type-checker verities consistent typing) or to apply custom domain-specific optimizations that a general-purpose optimizer can't do safely
