Comment by mellavora
5 years ago
This view: "Law already is a programming language."
always strikes me as so fundamentally wrong, and also very dangerous.
Goedel's incompleteness theory shows that an axiomatic system can either be consistent or complete, but not both.
Software is an axiomatic system. Human behavoir is NOT.
Law provides remedies for specific harms, such that vengeance becomes the right/duty of the state (which hopefully tempers it with justice)
Law thus needs room for interpretation and for understanding of the human. Thus the need for a judge. Thus a jury. etc.
As one man put it, "the letter of the law kills". Software is only the letter.
We all want clear, black and white guidelines on "good" and "bad". We sometimes look down on religions which seek to provide this.
For the love of $diety$, let's not make software that $diety$
I agree on all accounts, however I've always taken "Law is a programming language" or, maybe better, "Law is a program" as more of a metaphor. I see many similarities between law and computer programs, it's just that a law is a program written for humans (judge, jury, ...) to interpret, whereas a computer program is written for a computer.
Thus I think any attempt to translate a written law into something a computer can interpret as a failure, because the interpreter is not optional in the law. The interpreter is part of it and constitutes a vital piece of it, and without it written law does not make a lot of sense at all. Still, it is, in my view, a program which can be "executed", just not without a lot of context.
Actually, software can be as well "interpretable". It just means that the outcome is not "he has to be convicted because of X and Y" but instead "if X and Y are relevant then he should be convicted". Which means, software cannot automatically handle a case but it needs to be interpreted - however, the interpretation will be more formal and not so handwavy.
> Software is an axiomatic system. Human behavoir is NOT.
It really isn't though. When I write software I have to consider the different interpretations by the OS, browser, etc. and draft accordingly. Ditto for when I draft legal documents and need to consider the different interpretations by opposing counsel, a regulator, etc. As someone who drafts legal documents for humans and writes code for computers I can tell you first-hand the two processes are remarkably similar.
> Goedel's incompleteness theory shows that an axiomatic system can either be consistent or complete, but not both.
Goedel's theorem is about a specific form of incompleteness.
I think you'd have to provide some additional arguments why the theorem would be relavant in this context.
In other words: I don't think law as a formal system needs all the features that are preconditions for Goedel's theorem.
Similarly: Most proof assistants are very much usable without allowing arbitrary recursion.