Comment by friend_and_foe

That's really cool!

I was puttering around with the idea of a ricardian compiler for legalese, basically a decompiler for something like this that could compile a legal text into clear logical rules. This would aid in proof checking for legal documents to ensure that they're compatible with existing law, that there are no (unintended lol) loopholes and the like. It would also be useful if you wanted to create self enforcing legal documents that can be enforced deterministically by machines, such as collateralized agreements, and finally, even though someone would still need to know legalese, it could make the development of such agreements easier for people and lower the bar tremendously.

I wonder if anyone has built anything like that, if these guys have, or if anyone has built other interesting ricardian compilers.