Oh, this again. I suppose this looks relatively harmless, but I'm always wary of "law is like computer code."
The impulse to think this can strongly solve any real problem in the law is intuitively attractive, but I strongly predict this mostly never happens; it's the law's job to be intensely practical in the face of hard-edged "computer-like" rules.
If anything, you get goofy confusion about what things "are?" My go-to on this is always the "smart contract" -- which can be useful little bits of automated robot money moving code, but emphatically are neither "smart" nor "contracts."
I can assure you that the person who wrote this is very well aware of the subtleties involved with formalising the law. Law + Programming is an active research field (https://popl23.sigplan.org/home/prolala-2023), and it is very far away from anything like smart contracts, it is full of brilliant people who have no pretension of replacing the law with computers, but simply be helpers where they can.
Sure, I think I posted my response not because "it could never solve ANY problems," but instead "way too many non-lawyers, especially techy-non-lawyers, have the deeply misplaced idea that is a very important, perhaps THE most important, problem to solve in the law." It's just not very high on the list at all.
Maybe not for lawyers, no. But as a citizen I'm expected to comply with the law, with many many laws. It'd actually be nice if law was slightly more formally verifiable, so it would be easier for me to understand what to comply with.
Being able to break down clauses into more logical normal forms would probably greatly enhance the possibility of compliance.
For every bit of gained clarity, you'd also gain a ton of people like the "sovereign whatever" idiots who just love trolling, with the added negative of them having more "formal proof" of their untenable silliness.
This is a problem, but not one that Catala suffers from on a first reading.
Some elements of law are amenable to translation into source code, and indeed anyone working in fintech will probably have done that at some point. If the law gives a threshold for a tax allowance, for example, you need to encode that requirement in accordance with the law. Being able to mark up the text of each regulation should make it much easier to be confident you've not missed anything.
Trying to write non-financial regulation as code is pretty much doomed to failure. But to the extent that tax or benefits regulations set out numbers that we have to translate into code anyway, it's good to have that code be verifiable against the specific regulatory text.
> Hasn't Cyc impressively demonstrated just how incredibly difficult and costly it is to formalize even the most basic matters of daily life?
I would offer that the "cost/benefit" analysis for such a formalism exists on at least two axes: the concept domain which one is attempting to formalize, and the benefit (and/or size of consumers) of any such working system
I can wholly understand that trying to translate the entirety of English into a formal logic system sounds overwhelming. But to side with a sibling commenter, why not at least start with the tax code which is a personal pain point, has (presumably) a correct outcome for some cases, and is mostly algorithms-in-English
And then, for the consumer side: ok, if I snapped my fingers and Cyc existed and worked I struggle to think how exactly my life would change. If the formally-specified tax code existed and worked I wouldn't have to rage-upvote almost every comment on the annual tax hatred thread
I would even offer that an incomplete version could still be useful if one left "fuzzy" variables in the corpus, and said "welp, we can't define what a $Person is because of the hundreds of years of precedent, so you'll need an actual Judge for that". I don't meant to say that 50% of the corpus can be undefined variables, that's just silly, but I'd hope the tax code isn't built upon 50% undefined behavior, even if accountants want you to think it is
There have been many such attempts (e.g. NKRL by Zarri et al., also funded by EU). There are even societies that have been dealing with such issues for many decades (e.g. http://www.iaail.org). The formalization of law and language is only one of the issues. Like many previous attempts, this one suffers from the fuzziness of human language (even in the case of tax code). Fuzziness is not a drawback; it is what makes it possible to communicate efficiently in the first place. In order for us to communicate effectively, we need an enormous amount of tacit knowledge about our environment that our culture and life experience brings. If one tries to formalize the language, as in the present approach, one must also take this knowledge into account, down to the last detail (an "upper ontology" is by far not sufficient for this, and Cyc after decades is still not finished). And the tacit knowledge and also the moral valuation of the same change over time. And there are things like https://en.wikipedia.org/wiki/Sorites_paradox which stand in the way of a complete formalization. Lenat's 1990 book addressed many of the issues, but also his more recent talks are very informative where he demonstrates how they had to extend the Cyc representation language to cope with the problem, and why e.g. RDF triples are not enough.
- your compiler was AI-complete and adversarial and hated you
- your compiler was also not bound by any hard rules and could emit undefined behavior at any time
- your job scheduling and orchestration system was AI-complete and adversarial and actively hated you
- your runtime library had 50 different incompatible canonical implementations and can only be run by being forked by publicly-elected officials who blindly merge patches from bad-faith lobbyists
- the IDE is Microsoft Word, and the linter is a summer associate on their tenth cup of coffee
- you will inevitably get a non-technical client who thinks that the more times you have "notwithstanding the foregoing" in your code the more you can call yourself Web Scale
I like to turn this argument around to see how absurd it is.
Why not just take the existing law, and have a machine execute it in the style of a computer program?
We wouldn’t need judges juries or lawyers. You’d just type the specifics of your case and any supporting documents/evidence into the computer and a verdict would pop out.
Of course, the system could be used for other stuff too, like checking building code compliance or engineering soundness, signing off on military and police action, setting the executive branch’s priorities, and so on.
Not a lawyer. My thinking is very likely naive as I have no experience in this matter.
I see two potential issues:
- Picking evidences. "Evaluating" the law might need access to all the possible evidences that could exist, but that would certainly never be true, so you'd need someone to know which evidences to present. You probably cannot rely on some interactive process asking you such and such evidences because it would be presenting evidence that would trigger evaluations of chunks of laws. I would guess a lawyer with good knowledge of the law would probably be needed for this.
- Setting precedents. Wouldn't the "automated" law evaluation run into unprecedented cases all the time? You'd need someone to constantly issue a verdict on unforeseen situations all the time, and I guess you'd need a judge for this.
Maybe it could work on many "trivial" cases though.
Some people have argued that the fuzziness of the legal system can be a good feature for some reason, but you could always have a machine execute the law and a human make the final call. So you wouldn't need judges, juries, or lawyers, but you would need a team of legal shamans that sign off on verdicts
It is that the law would need to encode all the stuff I said, so it would need to be nuanced enough to replace all engineering, leadership and administration roles. (And also anything involving ethics.)
how many times have you fought in court to argue about "the spirit of the law"? I, for one, don't really care about this lang or "law is computer code" thing. just wanted to know lawyers life, I guess.
> If anything, you get goofy confusion about what things "are?" My go-to on this is always the "smart contract" -- which can be useful little bits of automated robot money moving code, but emphatically are neither "smart" nor "contracts."
They are contracts—just not legal contracts. One of many types of contracts in the world that are not legal constructs.
Software-interface contracts generally aren’t (cf. Design by Contract). The parent is correct insofar as the use of the word “contract” is not limited to contracts as defined by law.
It’s a contract (mutual agreement) between the client code and the implementation of the interface. The implementation fulfills certain obligations provided the client code fulfills certain other obligations. The interface defines what those obligations are. If the client code fails to meet its obligations, then the implementation of the interface isn’t bound to fulfill its obligations anymore either. The point is to think in terms of two parties, where the developer who is either using or implementing an interface takes on the role of one of the two contractual parties.
Oh, this again. I suppose this looks relatively harmless, but I'm always wary of "law is like computer code."
The impulse to think this can strongly solve any real problem in the law is intuitively attractive, but I strongly predict this mostly never happens; it's the law's job to be intensely practical in the face of hard-edged "computer-like" rules.
If anything, you get goofy confusion about what things "are?" My go-to on this is always the "smart contract" -- which can be useful little bits of automated robot money moving code, but emphatically are neither "smart" nor "contracts."