I think it'd be far more useful to work on tools for reliably codifying agreement and intent, in order to make it easier to generate and parse contracts agreed

I think it'd be far more useful to work on tools for reliably codifying agreement and intent, in order to make it easier to generate and parse contracts agreed by humans. The aim should be to restrict what it is possible to say in a contract, not expand the space to infinite possibilities as a Turing complete language does. I'm not convinced powerful languages will ever be suitable for this - the language used for contracts should be less flexible and powerful than human languages, not more - we attempt this with legalese and conventions associated with contracts already (they don't really use english say but a limited subset of it), why not take it a step further and define specific and incredibly limited axioms which can be connected to form immutable contracts with limited ambiguity and no room for error. Smart contracts assume that incredibly difficult problem is already solved and then start attaching money directly to the contract (why!), that in my view is far too optimistic about the state of software and the capability of humans to manage it.