mengwong

> 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.

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.

https://digitalcommons.law.yale.edu/fss_papers/4519/

https://repository.law.umich.edu/articles/29/

https://drive.google.com/file/d/0B8axPLLxhjQFWGc0ellBYTF3RnM...

https://twitter.com/paulg/status/1384422654195683328

> 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

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.

(TL;DR: yes, "law is code". And $10M of fresh funding says law should be open-source code, to be precise. Hackers wanted.)

Background: the "Rules as Code" movement is bringing software engineering practices to the drafting of law. https://govinsider.asia/inclusive-gov/four-things-you-should...

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...

(Why Singapore? Fun fact: it's the only country in the world whose prime minister has degrees in mathematics and computer science.) https://twitter.com/leehsienloong/status/595166789660647426?...

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

Market innovation: "Should it be done?"

Regulatory innovation: "May it be done?"

Today's model of contracting is fire-and-regret: spec out as much as you can of the next five or ten years, and when the world changes, litigate.

That's not very agile. Hart and Holstrom won the 2016 Nobel in Economics for pointing out the futility of the idea of a complete contract. http://www.economist.com/blogs/freeexchange/2016/10/science-...

What's the alternative? Hirschman remarked that your voice sounds loudest when you are closest to exit. https://en.wikipedia.org/wiki/Exit,_Voice,_and_Loyalty

What if we treated contracts as an iterated stream instead of an immutable invariant? What if every contract had a maximum term of one year, one month, one day? Power imbalances might be reduced precisely because nobody's locked in: it's a lot easier to break up when you're just dating. After the marriage you might let yourself go.

Software is eating law, but "law is code" is only the first step. Just as the historic transition from proprietary to opensource informs ideas like "Github for law", the historic transition from waterfall to agile will find its analog in the legal and business domains by changing the way we develop and deploy contracts, ultimately driving changes in economic relations.

Think about how "no-contract" phone plans have made the telco market more competitive, to the benefit of the consumer.

Think about how agile development means less software project failure, and less software project failure means less litigation between client and outsourced development vendor.

That's just one example of how litigation might be reduced. If better tools and languages mean that we can better transform our intent into specification, we might be forced to be clearer about what we actually do and don't agree on, we might be more honest in our dealings, there might be an actual "meeting of minds", and when things don't turn out the way we expect, rather than blaming the other party, which seems dysfunctional, we embrace change together, and agree to consciously work on the relationship, to improve the next iteration of the contract … which is due to be revised and renewed anyway, next month, not next decade.

Not a markup language: a full-blown strongly typed specification language with first-class functions, that supports formal verification / static analysis / model checking.

Those ideas, rooted in computer science, are what will set the next generation of legal drafting apart from traditional work.

Of course the language will be compilable to both natural languages and "smart contract" languages like Ethereum.

I justify these claims and work through your example in detail here: https://medium.com/@Legalese/code-is-law-is-code-4492c864f33...

Other thinkers, like Primavera de Filippi, have commented on "from code is law to law is code": http://firstmonday.org/ojs/index.php/fm/article/view/7113/56...

An archive of prior art is available at https://legalese.com/v1.0/page/past

We're working to build an opensource language called L4 with these properties. If you know, or want to learn, declarative programming (Haskell), dependent types (Agda, Idris), theorem proving (Coq), model checking (CTL*), rule systems (Prolog), modal logic, CCS, CSP, etc etc, join us! Computational thinking required, legal experience a bonus but not really needed. (evil laughter)

I am tracking instances of this genre at http://www.legalese.io/#priorart