what do you think of 3) the way we make law is deliberately "broken" such that inconsistent laws can be passed (with humans in the loop to sort it out) otherwise nothing would pass - if we could build a type checker for laws, active law would not type check and would be impossible to fix
This approach doesn't acknowledge that law is a dynamically typed language, to continue your analogy. It responds to societal concerns and emotional and frequently irrational reasoning. There's a saying bad cases make bad law and I think this isn't going to change any time soon.
Nevertheless dynamic languages can fail to typecheck. To continue the analogy:
try {
fair (trail);
} catch (e) {
if (e == InconsistentLawException) {
// Oops, divided by zero,
// add a tiny epsilon to the denominator and keep going
law += epsilon;
} else if (e == ClassCastException) {
// some types are more equal than others
settlement (trail);
} else {
// escalate to higher instance
mapReduce (court);
}
} finally {
// might silently fail if
// higher_instance == SCOTUS and
// SCOTUS.busy == true
sentence (trial) . await (appeal (higherinstance));
}
> This approach doesn't acknowledge that law is a dynamically typed language, to continue your analogy. It responds to societal concerns and emotional and frequently irrational reasoning.
The problem with this line of reasoning is that it leads down the wrong path. Formally verifying the consistency of the law cannot be done in practice because it has NP-complete problems inside of it. The amount of work it would take to create a legal code which is internally consistent and always yields an agreeable outcome is not feasible.
But it's foolish to go from there to the other pole where all the laws are overly broad and the only thing that determines whether you go to jail is prosecutorial discretion.
The formally-verified internally-consistent always-righteous version of the law is the unattainable platonic ideal. You never actually get there but progress is measured by whether we get closer today than we were yesterday.
> The amount of work it would take to create a legal code which is internally consistent and always yields an agreeable outcome is not feasible.
Is there something you can cite here? The infeasible thing to me is refactoring a pre-existing lawbase into something formally verifiable; if we could throw it all away and start over at the constitution, it might work.
The existing law isn't the underlying source of the complexity. It's that people want the complexity. They want killing to be against the law, but not if it was self defense, or you were under duress, or you couldn't reasonably know that your actions would kill someone etc.
You can easily pass a law that says all killing is illegal, but that isn't good enough. You either have to consider every possible thing that could happen in the universe and encode what should happen in each case into the law, which is clearly infeasible, or there will be things that can happen which you haven't considered ahead of time, and then you still have to specify something.
If what you specify is that unanticipated acts are illegal then everyone will be in prison. But if they aren't then it will be easy to find a provable loophole to murder. Neither of those is acceptable.
That's why we have judges. To address that. But that answer is still terrible because then you don't know what the law is until you're already in court. It's just less terrible than either putting everyone in prison or letting anyone get away with murder.
Which means the goal is to minimize the number of situations where that needs to happen, without causing the well-specified outcomes to be unrighteous.
This is one of the tools we are building at Open Law Library. Open Law Draft is a linter that finds common errors in draft bills right in Word as they are being drafted. Fixing the error before the bill becomes law is much easier than having to pass another law to fix it. Extending the analogy, Open Law Codify is essentially our compiler. We will be integrating the two so we can find more complex errors at the drafting stage rather than having to wait for the codification stage, as we do now.
Unlike what I think you are proposing though, our system must work with any law that is passed, not just laws we deem "correct". We simply write software that helps legislative bodies pass laws that are as close to what they deem correct as possible.
Then you want a safe incremental process that allows you to run unchecked code and annotate which code has been upgraded to meet the type checking standard - this is already done for javascript projects, you can introduce Flow to typecheck only the annotated functions in a file: https://flowtype.org/docs/existing.html
