The problem here isn't that we are missing a language for expressing laws. Indeed, DSLs for expressing legal axioms don't really exist, and I expect that formal

The problem here isn't that we are missing a language for expressing laws. Indeed, DSLs for expressing legal axioms don't really exist, and I expect that formal verifiable languages will be created, but even when they are, the problem is not an inability to express laws, the problem is how to map them to entities in the real world. To give only a single example, "what is admissible evidence?" Assume for a moment that we have solved the "what is admissible evidence in this context" problem. Now you have a giant list of pieces of evidence, testimony, etc. How do you prove chain of custody? The legal system is utterly blind to the world, its agents are intentionally blinded to much of the information, and practically blinded to others. Even with modern surveillance the amount of uncertainty that is present in many legal cases is substantial, and machine learning won't help you here, because every legal case is a one off. I'm sure someone will try to create a statistical guilt detection net despite the obviousness that it will inevitably produce unjust results. If you want laws to be written in formal languages, you need a system for defining formal semantics for the entities and relations that their abstracted axioms describe, and things like OWL and RDF are not sufficient, because they only provides the hypotheses, not the evidence. You can assert that evidence subClassOf admissible-evidence, but you need proof that the assertion is valid that can be checked by multiple parties (or anyone with the desire to do so). The one-off nature of many cases often means that you can't go out and test the hypothesis again. These are hard measurement problems, and we don't have a good language for describing them, and how the measurements themselves are governed by the legals system. That said, being able to bootstrap simulate court cases with juries drawn from the population would already be a massive win for interrogating laws and their implementation and enforcement. Similarly being able to simulate new legislation to reveal loopholes would be fantastic, though I doubt politicians would enjoy that. There is quite a bit of data, but I don't think it is particularly amenable to the current fads in machine learning. Amusingly people complain that we'll never be able to write down all the axioms, yet someone wrote down all the laws. Economically unattractive due to a tragedy of the commons certainly, but at the end of the day someone is going to have to write down all the axioms, one way or another. Maybe modern machine learning techniques could be used to generate the axioms for humans to review?