> Most people today don't write code for safety critical systems. The abstract mentions they already uncovered a "bug" in an active law by rewriting it in their language, so it could be an immensely helpful tool for finding edge cases and loopholes in that mess.
I'll give you an example from a field that I (unfortunately) have a reasonable amount of experience of where the law and contracts are supposed to be interpreted 100% literally like an algorithm: structured finance (eg the subject matter of the 2008 financial crisis). The prospectus of a structured security like a mortgage bond is typically a hundred or more pages of very dense legalese that was worked on intensively by highly-specialised lawyers and bankers for months. Its intent is to set up a small special-purpose company with strict rules on how it operates down to the last penny and zero discretion. This allows investors (in theory) to understand how the bond will perform.
The opening chapter of my introductory textbook on structured credit analysis says the author (who has been part of those teams for years and has worked on hundreds or possibly thousands of bonds) has never read a bond prospectus for a structured security that does not contain serious drafting errors. I personally worked on a bond for months and read, edited and commented on the bond model and prospectus hundreds of times. We certainly were trying to make our prospectus as simple, clear and loophole-free as possible. Then a few years after it launched we discovered we had made a big mistake in drafting it that had gone unnoticed by me, the expert bankers and lawyers and all the investors so far. Luckily we were able to fix the problem without negative consequences. There is literally no chance that this error would have been found or solved by a formal system and if anything it would actually have been worse.
Some things are complex enough that they are just very hard to do. The existing system allows for that by having a rigorous process of dispute, interpretation and argument to decide complex questions post facto.