[Rochus]

That gets to the heart of the matter. I have studied computer engineering and law as well. Statements like "Verilog allows programmers to draft circuits, Legalese's L4 will allow programmers to express law" demonstrate naivety to the real challenge. The authors should take a closer look at the disillusionment that has arisen after fifty years of rule-based knowledge representation and inference.

[tgbugs]

Consider also the disillusionment that a significant portion of the population feels when confronted with the nearly 1000 years of rule based knowledge representation that is common law.

Maybe a good law would be that if you can't be arsed to write the law in a formal language, or can't figure out how, then it shouldn't be a law in the first place :)

[Rochus]

Human language, and therefore laws and court decisions written in human language, work because members of society share an enormous amount of tacit and background knowledge and share similar value standards based on their cultural history. The fact that all this information can be assumed and does not have to be explicitly specified is what enables us to communicate efficiently in the first place. If you had to specify the actual knowledge content in order to fully understand facts and draw computer-aided conclusions, the effort to write or read these texts would be almost infinite. The idea of writing laws and contracts in a "programming language" thus misses (once more) the real problem. And beyond that works like those of Gödel or Wittgenstein showed other limits of formal systems long ago.

[amusedcyclist]

The limits of formal systems are nowhere near being approached by law, which is generally pretty simple but written in obtuse language or full of exceptions that exist purely because of the fact that its very hard to change laws. Legal communication is precisely the opposite of efficient. That being said, some types of law are obviously less amenable to being described in formal language (like laws concerning murder or situations involving complicated human - human interaction). But that is absolutely not true for the average contract , which constitutes most of the legal industry's revenues and time. In that case the only problem is that laws are pointlessly complex. As another example, we'd all be a lot better off if taxes were formulated as a program.

[afarrell]

> we'd all be a lot better off if taxes were formulated as a program.

They are. It is called turbotax and it is built and maintained by Intuit, who also has powerful lobbyists.

I think what you want is a non-spaghetti open-source software program maintained by a governance structure which is both

A. Competent and communicative.

B. Accountable to the same public which is in charge of doing performance reviews for the current legislators.

[Rochus]

Laws are neither complete nor free of contradictions, and they don't have to. They are the result of a consensus among members of society that has grown over centuries. Democracy is significantly based on trust, transparency and comprehensibility. Legislation is subject to the permanent challenge of finding a balance between regulatory density and manageability. And even if it were socially feasible to rewrite all existing laws, to formalize them, and to massively increase the density of rules: the set of rules will always remain discrete, and it is a naïve assumption to want to fully capture the continuity of human action with a discrete set of rules; there will always remain an unspecified residue that requires human judgment. Striving for a perfect system fails merely because there is no universally accepted definition of a perfect system; and societies in which an attempt was made to realize the utopia of a perfect system were usually totalitarian or became totalitarian in a short time.

[cies]

> Human language

You mean natural languages. Formal languages (of which programming code and math are examples) are also human languages, but more well defined and usually designed by few (opposed to emerged from usage by many).

[Rochus]

See e.g. https://en.wikipedia.org/wiki/Language.

[perl4ever]

How do you feel about building codes?

[tgbugs]

Roughly the same way I feel about HIPPA certification. Except that there is an additional interaction of building codes with zoning laws that leads to inflated housing prices in the US. Also, if you want to know if the house was built to code, you have to inspect it yourself, or at least be on site frequently enough to keep the trash from being stashed in the dead space.

There is of course a separation between safety and standards that is hard for laws and codes to grasp. The separation between intention and results is one of the reasons why you want these things explicitly defined as part of a formal specification for a law, it makes it possible to determine whether it is having the desired effect, and if it is not it could .e.g trigger a clause removing the code from being in effect. Rent controls would be a perfect example for this, though the whole point of my argument in my top level response is that trying to measure whether rent control is effective is the hard part (every serious study of rent controls shows that they are not).