> As Merigoux explained more fully on his blog, this project became possible because the French government open-sourced the code that they use to calculate residents’ taxes, which was written in a domain-specific language called M, but they didn’t release the compiler that would have been needed to actually run any code written in that language. MLang is a compiler for M code written by Merigoux, and it has two special features: it translates the tax calculation function to Python, and it enables formal verification of features of the tax calculation using an automatic theorem prover called Z3.
Sure, but the intended user for a lot of this stuff isn't the lawyer – it's the end-user who's glad to have an alternative to the lawyer! Like, owning a bicycle means I don't need to call a taxi for some trips. Not all trips, just the local ones, but that's a lot of my trips.
Free access to law, and software for filings like afterpattern.com, that's the boring stuff that lawyers don't want to do and I don't want to pay for, so win/win. And that's all part of the larger vision of computational law that Legalese wants to help realize. Thanks for the good wishes and I hope to deliver on the vision, we've been at it for five years and will probably be at it for another ten before we start seeing results percolating into the real world.
> In 2008 I spent a month writing a web-based system for managing all YC's funding documents. With one click you could get an instance of the latest docs, prepopulated with all the startup's info from our database. The lawyers quietly ignored it and kept using Microsoft Word.
Others have said in the comments that doctors and lawyers are "the last, most powerful guilds" remaining. On the one hand, it's easy to call for "the end of lawyers". (The Legalese website says that sort of thing as a provocation, a way of staking a flag in the sand.) On the other, it's likely that society will always define a special role for the white-collar warrior, the champion of the courtroom; for high-stakes, once-in-a-lifetime situations, you want expert human hand-holding.
In books like https://www.amazon.com/Future-Professions-Technology-Transfo... Richard Susskind offers a more nuanced middle ground. Look at medicine: together, the Apple Watch, WebMD, DirectLabs, home glucose monitors, and home blood pressure monitors (let us never miss an opportunity to say "sphygmomanometer") allow millions of people to do for themselves what they used to need a doctor for. In turn, that lets doctors focus on more high-value work.
Suppose we distinguish quantitative and qualitative reasoning: numbers belong to the former; legal and logical problem-solving to the latter.
Quantitative reasoning went in-house when spreadsheets (the original killer app) landed on the PC: now millions of people do for themselves what a couple of generations ago used to be the domain of the accountant, the bookkeeper, the finance specialist.
What would "spreadsheets for law" look like? If tools emerge that allow laypeople at home and in business to explore for themselves simple questions like "what is the deadline for me to do X", "what things am I required to prepare ahead of that deadline", and "how do I get out of doing Y", frankly the lawyers might breathe a sigh of relief so they don't have to keep annoying people by answering "it depends". There's plenty of low-hanging fruit out there like that which makes people's lives better. Software like docassemble.org and startups like afterpattern.com are exploring these possibilities. Farther into the science-fiction future, researchers in France did a lovely demo, basically fuzzing the tax code to find a sploit that deserved to be patched. https://blog.merigoux.fr/en/2019/12/20/taxes-formal-proofs.h...
One final point: people who argue for the necessity of discretion and the desirability of vagueness and ambiguity tend to have, in the past, benefited from such discretion. But there are less privileged people out there who have been on the sharp receiving end of discretion, and they might prefer a little less discretion and a little more algorithmic, explainable, deterministic fairness!
For folks who happen to be unreasonably interested in this stuff: there are research engineer positions open at the Centre for Computational Law at Singapore Management University where the bulk of the R&D is happening, in partnership between Legalese and the university.
TL;DR: Move to a tropical island, get paid to write open-source software, and explore the arguments being made in this thread in way more detail than you dreamed possible. DM me on Twitter, @mengwong
Sorry about that! I'm adding a link to the PDF version which I think is tagged for accessibility. So you should be able to click on the image and go to the PDF. Give me a while, though, am fighting with Jekyll.
You're quite right. Garbage in, garbage out. And if the cost of generating garbage goes down, we're going to get a lot more of it! There are definite risks in misinterpretation and complexity and cruft. As Genesereth quoted:
The Lord's Prayer is 66 words, the Gettysburg Address is 286 words, there are 1,322 words in the Declaration of Independence, but government regulations on the sale of cabbage total 26,911 words.
So, we will have be on our guard. The hope is that if the rules are open and machine-readable, we will be able to counter with software that sides with the user and helps to mount the sort of response that in the past was only available to corporations with very deep pockets.
One intriguing approach is to submit test cases: concrete scenarios, or traces of events, that should result in certain desired outcomes. A diverse range of people in different circumstances could be collected in a comprehensive test suite. If the contract/law passes the test suite, you're good! You can imagine two legislators from different parties with different constituents and concerns, each bringing their set of test cases; and when the negotiated compromise passes enough tests, they proceed, without ever actually reading the text of the bill, lol.
The premise: the judiciary is one source of authority; the legislature is another. If we treat contracts and laws as executable programs and specifications, we want to find bugs at compile time, because handling exceptions at run-time is called "going to court".
How do we find bugs at compile time? Static analysis. Formal methods. Formal verification methodologies (Lamport's TLA+, MIT's Alloy) applied to contracts and laws make it possible to SAT-solve for loopholes ("sploits") that violate LTL/CTL specifications. Once law is code you can go full white-hat/black-hat. Automate the fuzzing. https://www.theatlantic.com/technology/archive/2017/09/savin...
Maybe we don't always want "law as code" ... for, say, criminal law. Judicial discretion is important. Human judgement matters. Though if an overworked public defender can only spare two hours out of the hundred you deserve, the robolawyer starts to sound more attractive. What if we send Watson to law school? If you're hunting for a way to stay out of jail, wouldn't you want Deep Blue and AlphaGo to help you find it?
https://www.nytimes.com/interactive/2019/01/31/us/public-def...
There are plenty of black-and-white areas where the rules don't invite human interpretation: mostly things to do with finances -- like how DoNotPay.com can help apply for unemployment. Even in those domains, there are deep, deep pockets lobbying against the kinds of freedom (as in speech, and as in beer) that "law as code" promises.
https://www.propublica.org/article/inside-turbotax-20-year-f...
But, you ask, what about the knowledge acquisition bottleneck? Ah, yes, the AI Winter. Ontologies (SUMO, OWL, UFO-L), visual modeling notations (BPMN, DMN), and a new generation of tools (Flora-2, Protégé) take a new whack at that problem without going anywhere near machine learning and neural nets, which typically lack the nuance you need when every comma counts.
https://www.bbc.com/worklife/article/20180723-the-commas-tha...
Spring is coming. The vision for computable law, as laid out by Michael Genesereth at Stanford's CodeX Center, is for software that does for legal reasoning what the spreadsheet does for quantitative reasoning. (Who's Michael Genesereth? You've heard of Russell & Norvig's textbook on AI. He was Stuart Russell's Ph.D advisor.)
https://dl.acm.org/doi/10.1145/1165485.1165517
Is there any money in this? Hell, yes. In the US, DoNotPay is running a pitch-perfect Christensen disruption playbook. Outside the US, the EU has issued a half-million-euro tender for exactly the Rules As Code thing mentioned above: machine-readable-and-executable regulations. See section 1.4.2 of the PDF at https://etendering.ted.europa.eu/document/document-old-versi...
Oh, and as of last month, Singapore has just thrown $10M behind a project to turn the "law as code" vision into open source software that you can clone off Github.
I've been researching computational law since 2015, and a picture of the future legal tech stack is coming together in my head: open-source, open-standards, laws and contracts drafted in a domain-specific language from the start; libraries of clauses, linters and interpreters and unit testers and theorem provers built into the IDE, that find bugs in contracts in real time as you edit; compilers to English and other languages; model-driven architectures that flow from the specification to the app.
Once that legal stack is downloadable and accessible to the geeks of the world, then, as Joshua Browder would say, DoNotPay a law firm thousands of dollars just to copy and paste a Word doc out of their library. The law firm is not the customer -- as Atrium proved, expensively.
To help move this stack out of my head and into Github, the SG government is funding the development of open-source software targeted to real-world use cases, for drafting rules and contracts in a DSL. They've approved a grant for my small team (hi, Alexis! <3) to hire people to make it happen.
https://www.thetechnolawgist.com/2020/03/31/legalese-singapo...
If you're in a position to move to Singapore (whenever air travel reboots) ... and have skills in obscure but powerful technologies (or want to gain those skills) ... and want to help design a language that could be the basis for the next iteration of the legal industry ... we're hiring:
https://computational.law/hiring
> As Merigoux explained more fully on his blog, this project became possible because the French government open-sourced the code that they use to calculate residents’ taxes, which was written in a domain-specific language called M, but they didn’t release the compiler that would have been needed to actually run any code written in that language. MLang is a compiler for M code written by Merigoux, and it has two special features: it translates the tax calculation function to Python, and it enables formal verification of features of the tax calculation using an automatic theorem prover called Z3.