I think these developments should be done with care and cognizance of the user. I worry that formalism may have trouble scaling and interacting with user intent. LLMs will (and already do in my experience) construct a formalism for your application that may be provable to some archetype -- but separate from reality and separate from your conception. The Claude user experience of rulings is already at a cultural limit among users -- the excitement over the linguistic 'improvements' of the Opus 5.5 release are a case in point. Formalism is only one axis here and usability is another. This could be a problematic development if done lopsidedly.