> but lisp syntax... is less legible than TLA+ imho. I've developed theorem provers with more natural syntax, and in retrospect simpler grammars are better. Th

> but lisp syntax... is less legible than TLA+ imho. I've developed theorem provers with more natural syntax, and in retrospect simpler grammars are better. The stone cold truth is that most people aren't interested in using theorem provers directly; instead, they're programmatically generating queries. Simpler grammar = easier to generate, and that out-weighs direct usability. In my next system I'll be supporting both types of grammars in the parser.