The law doesn't specify anything as precise as an algorithm. The law has multiple statutes, codes, precedents etc with overlapping applicability. Then in a particular case these are tried and humans come to a decision.
Trying to pretend it's precise like a computer algorithm is I think a really big problem.
The reason I posed those particular questions is that if you try to make this answer the questions you rapidly approach a level of complexity similar to the existing legal codes and still don't have something that could automatically be evaluated.
> The law doesn't specify anything as precise as an algorithm. The law has multiple statutes, codes, precedents etc with overlapping applicability.
Again, I think you're arguing about something that the paper doesn't claim to do. It doesn't claim to formalize "the law" as a whole. It claims to formalize part of a single section of a single statute. That specific statute describes precise rules into which you feed boolean and numeric data, and the application of which rules spits out boolean and numeric data. These rules are written specifically so that they are not ambiguous, so that anyone given the same input data would come to the same output conclusion. That's an algorithm.
What is indeed ambiguous are questions of ownership: Did you own a certain property for two years within a five-year period if for part of that period it was co-owned with a friend who then became your spouse and then later divorced you and got the property? But again, this is not what the paper claims to decide. This is something that the algorithm in the paper, and the algorithm of this specific section of the tax code, takes as input as a boolean flag.
> The reason I posed those particular questions is that if you try to make this answer the questions [...]
But again, you do not try to make this answer these questions. And the paper never claims that it does.
The tool described in the paper does not contain a function like "given THE ENTIRE STATE OF THE REAL WORLD, compute whether I owned such-and-such property for two years in a five-year period". The tool described in the paper only contains a function like "given a boolean flag modeling MY CLAIM to have owned (or not) such-and-such property, compute a number for me".
Your reasoning for having owned (or not) a certain property is not checked by the tool described in the paper. It takes your claim about property ownership as a boolean flag and says "well, if you are really sure that your claim is correct, then your tax liability is such-and-such". It doesn't claim to check whether your claim is correct.
Sure, but the problem is then it's not very interesting. There are lots of real-world systems already that do this with existing laws and existing programming languages (eg in the UK where I live the the tax service has a free web filing system where you fill in your tax return online, it checks it for correctness and tells you how much you owe or are owed (if you have overpaid).
Trying to pretend it's precise like a computer algorithm is I think a really big problem.
The reason I posed those particular questions is that if you try to make this answer the questions you rapidly approach a level of complexity similar to the existing legal codes and still don't have something that could automatically be evaluated.