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