It's a mistake to think that only things which are "absolute" can be logically programing. Take this silly example:
> If x is a good person they can go to heaven. Unless they were born on Feb 29th. The previous restriction is lifted if the year is a prime number. The counting of the year is Julian. The destination of heaven is replaced with hell if at least 5 people are on mars.
As the article shows, exactly existing law is fully of "whoops, you better keep on reading to find that override" situations like the above. Formalization still helps by putting all branching up front rather than with the the moral equivalent of COME FROM statements. And that helps whet there or not "good person", "heaven", and "hell" are well defined.
...The responses to this prreprint make me think no only do HN readers not understand the law, but they don't understand programming well either. :/
I agree with this but I also want to see someone try and fail and help us learn from it. This is really one of those untouched territories and there is reward in pursuing that regardless of the end result.
>Software is an axiomatic system. Human behavior is NOT.
I am not aware of any system of law that covers all possible human behavior. Common law systems theoretically could because part of the determination of what is covered is up to the courts, thus when you have a new human behavior it is uncertain if it is covered or not until you take it to court, but in a Napoleonic system the coverage of the law must be explicitly stated.
Thus Napoleonic systems would try for consistent but not complete.
I assume you refer to his results regarding axiomatic systems for arithmetic on natural numbers? If a law attempts to capture this, then, sure, it's problematic. But I don't that's very common.
From what I've seen, formal methods for legal systems would take the "facts" of a case as given (assumptions), and deduce legal consequences of those.
