My point is mostly that often, when it comes to law, lay-people talk about what they _wish_ the law was, rather than what the law actually is. And yeah, lawyers can be wrong too. But sometimes, things that seem common-sense aren't actually legally correct, and this is one of those cases. It does feel silly that a messaging company can threaten to sue over an unrelated software package, but that's just part of how intellectual property law works.

> My point is mostly that often, when it comes to law, lay-people talk about what they _wish_ the law was, rather than what the law actually is.

That is why the law should be formalized such that correctness proofs for argumentations can be given and in doubt even be checked independently by a computer. Exactly because of the possibility of different opinions and wishes, coming up with such a high standard should be considered a maxim.

My background is in 20th century Anglo-American philosophy, which spent a great deal of time seeing how far one can push formalization or quasi-formalization of interesting concepts. I wish I had a good capsule version of why I think this won't work, but it won't. Formalization is a tool, and an important one, and there probably are areas where a more formal approach to law could pay off. However, attempting to remove all ambiguity, vagueness and subjectivity is liable to leave you with paradoxical results.

Perhaps you could start with this: to formalize any set of laws and criminal procedure similar to the actually existing law, you'll have to define knowledge, and that is a quagmire (http://www.unc.edu/~ujanel/Gettier.htm--you don't have to read the entire paper, but at least read the first section for a feel of how nasty the project gets. If you need more background, here is the description of what the Gettier problem is: https://en.wikipedia.org/wiki/Gettier_problem).

I just read about the Gettier problem: In my opinion one should better model knowledge as some kind of estimators for probabilities and being justified on some statistical criterion. This should in my opinion avoid the whole Gettier problem (but perhaps introduce some completely different ones?).

I prefer the definition of knowledge given by Orson Scott Card, if I'm not mistaken: something you believe to be true. It doesn't have to be justified and it doesn't even have to be true - you just have to believe it.

I know that the Moon is about 400,000 km away from the Earth. I have never measured the distance and I haven't even tried to check if it's plausible: I read it somewhere and accepted it as such.

While I can appreciate this sentiment, I'm also not sure that removing any sort of interpretation is a good idea. Look at the horrible impact mandatory minimum sentencing has had, for example. Flexibility can be bad, but it can also be very good.

> Look at the horrible impact mandatory minimum sentencing has had, for example. Flexibility can be bad, but it can also be very good.

That is rather an argument why in doubt one should not put such harsh punishments into the law - a thesis which I support.

There are a near-infinite set of complexities in legal cases. Trying to create a formalism for such laws would require solving the entire field of ethics to decide at which point something might be considered "reasonable doubt".

> to decide at which point something might be considered "reasonable doubt".

As far as I know this is a mostly done problem (google "statistics").

I don't think you understand what "reasonable doubt" means in a legal setting (Google "reasonable doubt").