I attended a computing conference in LA a few years ago where someone presented a paper that turned legal phrases into code, and was able prove theorems from it. She suggested it was a way to mathematically look for "bugs" in the legal documents.

I thought it was the most fascinating talk in the conference.