> Common Lisp is poorly suited to proving that a large program obeys certain strict rules As I'm sure you know, a Lisper would probably design a domain specifi

> Common Lisp is poorly suited to proving that a large program obeys certain strict rules As I'm sure you know, a Lisper would probably design a domain specific language that was well suited for such proofs. One of the projects I'd like to get around to one day is a Lisp hosted general purpose DSL[1] based on predicate transformer semantics[2] that combines writing specification and program text into a single interactive experience. Think something along the lines of smartparens[3] strict mode, where the editor doesn't allow you to make an edit that will violate the count("(") == count(")") invariant and you modify the tree structure with operations like slurp and barf, but a bit more general. [1] Haha, I know. [2] https://en.wikipedia.org/wiki/Predicate_transformer_semantics https://en.wikipedia.org/wiki/Predicate_transformer_semantic... [3] https://ebzzry.com/en/emacs-pairs/ https://ebzzry.com/en/emacs-pairs/