Another problem is that it will probably increase the proliferation of strict liability offences.

The fact that a law is internally consistent and free of loopholes does not necessarily mean that it is a good law but an algorithmic approach to creating such laws risks making their creation too easy so that we end up with a large body of law that can't be argued against because it has been 'proven' correct.

I'm reminded of a remark that Donald Knuth made regarding a piece of code. It went something like this: "Be careful if you use this, I have merely proven it correct but not tried to run it."

I'd urge people to consider their experience writing unit tests. It's not uncommon for me to write a test that my code fails, not because the code was wrong, but because my test was wrong. The same applies to proofs. You can prove that your code does something, but that doesn't prove it does what you wanted. It's easy for us to understand, but I could imagine lay people misinterpreting it.

>> Judging by how most people write code today, I find this idea terrifying

> 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.

> 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. 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.

There is no chance that a formal system wouldn't have revealed this bug? Static analysis and simulations wouldn't have helped?

> Some things are complex enough that they are just very hard to do.

I agree with this wholeheartedly. Engineers have the ability to automate some very complex issues. But there will always be a class of issues beyond automation, simulation, analysis, etc. and we just have to accept that the only way to solve them is with slow, hard, error-prone work.

Do you think that smart contacts could be useful in this area?

Not smart contracts exactly but there is a specific part of each bond called the waterfall (basically specifies what happens with all the cashflows under different circumstances and is a little bit like an equity cap table plus liquidity preferences). I've always thought there should be a dsl specifying the waterfall that can be used for the bond model and used to generate the legalese in the prospectus. A common problem is the bond model doesn't match the prospectus and that problem would just disappear. I intend to do this as a research project if I ever get time (it's been 12 years since I had the idea to do this so it may never happen...).

If I understand it correctly smart contracts are just another piece of software combined with some blockchain magic. If you can't prove a piece of code is correct, wrapping it in a trendy buzzword won't make the code more correct.

Maybe I'm wrong, but I don't know how decentralization would change anything other than adding safeties against manipulation if done right.

That line in the summary is a bit misleading. The authors didn't find a "bug" in any law - instead they found a corner case that wasn't coverred by an online tool hosted by the French government to estimate family benefits under French law:

> After close inspection of the OpenFisca code, a discrepancy was located with the Catala implementation. Indeed, according to article L755-12 of the Social Security Code, the income cap for the family benefits does not apply in overseas territories with single-child families. This subtlety was not taken into account by OpenFisca, and was fixed after its disclosure by the authors.

Here's the pull request for their fix to the benefits simulator: https://github.com/openfisca/openfisca-france/issues/1426

There's a real slippery slope issue here too though, for several reasons, that I'd expect would lead to overuse.

It's a fancy new thing that will be branded as helping to avoid mistakes, reduce legal system costs, increase consistency, etc.

So, it will be applied to existing laws more generally than the abstract suggests it should be.

New laws will be made with this in mind, increasing application regardless of whether the new laws are actually literally interpretable.

It will become entrenched and hard to remove as allocated funds to pay people to do the same jobs disappear.