Thirty Years of Legal Informatics
The legal informatics industry is older than most web developers working today.
Why the Status Quo causes pain
So something has to change. Programmers to the rescue. But most web developers are used to playing with tech that’s only been around a years, even months. Quick hacks are good enough – after all, what’s the worst that could happen? Reload the page, if it didn’t work, it’ll be obvious.
Contracts are different. Once executed, they don’t change. Parties can turn hostile – as TheDAO discovered. So “move fast and break things” does not apply. Respect the prior art. There’s a lot of it.
- Contract Formalisation and Modular Implementation of Domain-Specific Languages, Tom Hvitved's 2012 PhD Thesis, is a key inspiration for Legalese. The first chapter offers a comprehensive survey of prior art in contract formalization.
- Harry Surden's Computable Contracts, 2012
- Nick Szabo, Smart Contracts, 1997
- Stanford's Computable Contracts Initiative
- The Ricardian Contract, 2004, relates legal language with executable code via parameterization
- Smart Contract Templates by Christopher D. Clack, Vikram A. Bakshi, Lee Braine, 2016 describes goals very similar to ours
- The Representation of Legal Contracts by Daskalopulu & Sergot
- Using the Event Calculus for Tracking the Normative State of Contracts
- Abstract Specification of Legal Contracts, Prisacariu & Schneider
- Towards a Formal Language for Electronic Contracts describes CL
- Challenges in the Specification of Full Contracts
- Analysing Normative Contracts by John J. Camilleri
- Many other publications by Gerardo Schneider in association with the COSoDIS project, using CL for automatic conflict detection
- c-o diagrams/
- Contract as Automaton by Flood and Goodenough
- Abubkr Abdelsadiq (2013) at Newcastle published a toolkit for model checking contracts, using SPIN / Promela rather than Uppaal
- Regarding model checking, see also FormaLex linked elsewhere on this page. They published about formalizing the Argentinean Customer Protection Act, in 2017.
- Toward Machine-Understandable Contracts, 2016, by Sudhir Agarwal, Kevin Xu, John Moghtader at Stanford, defines CDL, Contract Definition Language (implemented in Prolog), part of work at the Stanford Computable Contracts initiative
- These Are Your Rights: A Natural Language Processing Approach to Automated RDF Licenses Generation
- A Domain-Specific Language for Normative Texts with Timing Constraints
- Reasoning about Partial Contracts
- Attempto Controlled English is an example of a formal/natural hybrid language which could be a compiler target.
- Semantics of Business Vocabulary and Business Rules is a hybrid formal/natural language for business operation and compliance which could also be a compiler target.
- Realization of Natural Language Interfaces Using Lazy Functional Programming
- RuleML e.g. Modelling Contracts Using RuleML
- DMN: Decision Model and Notation
- FEEL: Friendly Enough Expression Language
- LegalRuleML is an OASIS Technical Committee.
- W3C POE WG
- The Estrella Project attempted to "develop and validate an open, standards-based platform allowing public administrations to develop and deploy comprehensive legal knowledge management solutions."
- LKIF, an OWL, came out of Estrella.
- Formal Methods as a Link between Software Code and Legal Rules
- CLACK at UCL (clacklang.org), which may inform R3's work (see slides)
- Lexifi's MLFi was one of the earliest commercializations of financial contract formalization
- Algorithmic Contract Types Unified Standards (ACTUS) breaks down financial instruments into a manageable number of cash flow patterns: so-called Contract Types.
- Joe Dewey's essay on ContractCode, April 6, 2016
- Codex by Pax is a scripting language for Ethereum; in concert with Pax Directory
- Restatement by Jason Boehmig, Tim Hwang, and Paul Sawaya. (intro essay; see also Modeling - Background Reading)
- CommonAccord has some early thinking online.
- Law.MIT.edu takes a social-science approach to examining law: see Dazza's video.
- Guido Governatori has published extensively on defeasible logic.
- There is a W3C Working Group on Permissions and Obligations Expression which has published an ODRL Vocabulary and Expression draft standard.
- This is close to RuleML and LegalRuleML.
- The urge to formalize goes back at least as far as Leibniz.
- Bridging the gap between expectation and reality compares smart vs traditional contracts.
The idea of developing calculi for the legal world goes back to at least the 1980s, when the British Nationality Act was encoded in Prolog. See also FormaLex for an LTL-compatible deontic approach. A recent (2015) survey can be found in Logic in the Theory and Practice of Lawmaking.
The following can be read as a quick introduction to corporate structures and legal agreements for the working programmer.
- A corporation or a company may be completely represented as a data structure. More precisely: those aspects of a corporation which have to do with its nature as a legal entity may be captured by a data structure comprising state information. Over time, the state changes: as a corporation acquires directors, investors, employees, ESOPs, and other contractual counterparties, the data structure evolves. Such state changes to the data structure are analogous to git commits or to database transactions.
- Each major change in the evolution of a corporation may be modeled with the language of git releases and tags. Each intended change may be modeled with the language of issues and milestones. What, in git, we call a remote origin master corresponds to, in corporate law, a state registry of corporate details.
- Alternatively, these changes can be modeled with a bitemporal database—ACID CRUD. Either way, formal structure can apply.
- Changes to the corporate data structure are formalized in shareholders’ and directors’ resolutions, and by executed contracts. Putting signatures on paper is execution. Legalese talks about corporations. Similar modeling is also needed for trusts, non-profits, etc.
Modeling Execution (as in signing)
- Automated legal reasoning is a hard problem. Corp sec is possibly the easiest practical domain of application.
- Corporate paperwork often requires signatures on multiple documents. Related documents may be modeled by a directed acyclic graph: if a prerequisite document is not signed, its dependents are invalid.
- The DAG may be computed algorithmically. The paperwork may be generated automatically. With the advent of electronic and digital signatures, the execution of such paperwork may be managed online. Reminders may be sent automatically. If execution is in progress, the state of the dependency graph may be examined in fine detail by parties at any time.
- Execution may require the observation of certain formalities which shade into the content and structure of the contract. For example, a novation needs to have n_orig + n_new parties involved. A deed needs to be phrased in a particular archaic way (the “Stevie Wonder phrasing”) to be valid.
- A particular document may be a collection of resolutions, or a contract.
- Knowledge-Based Systems and Legal Applications
- Stash has self-executing smart contracts
- Ethereum is obviously all over this.
Of course law firms think clarity and end-user empowerment are terrible ideas
You would too, if you had a busy contract drafting practice on the one hand, and an even busier dispute resolution practice on the other, both billed by the hour!
Modeling Contracts: Drafting
While execution is concerned with the relations between contracts, and does not look into the body of a contract beyond the parties and the signatures, drafting is concerned with the content of contracts.
- Natural-language contracts often look like somebody trying to program without knowing any programming languages.
- To a programmer, the structure of a contract reveals familiar ideas. The preamble is a high-level comment block that may declare assertions. The definitions section declares variables and constants. The conditions precedent define, well, preconditions. The main clauses describe the happy path. The breach/damages clauses handle exceptions. The term clause defines a timeout. And so on.
- Few contracts use basic structured programming idioms. Most complex contracts read like spaghetti code–object/machine code whose control flow jumps all over the place, from one clause reference to another.
- Some contracts are (inadvertently or deliberately) obfuscated.
- Imprecisions abound. Bugs result.
- The idea of drafting agreements in a high-level language is not new: in many situations, parties negotiate a term sheet; once agreement is reached, they hand it to a lawyer to expand into definitive documentation, which the parties sign without reading; the long-form version is only read when it is being executed in the context of conflict resolution.
- If a contract could be written with the rigor of a software program, it would be amenable to formal methods and other value-adds, like graphing and scenario visualization.
- A Legalese contract–one written in a high-level language–could be compiled to a natural language. Obviously, the situation calls for a compiler, perhaps paired with a domain-specific language.
- Such a compiler would produce natural language contracts that were backward-compatible with the legacy industry. Such backward-compatibility is valuable for lawyers, judges, and laypeople who aren’t able to read the high-level DSL.
- A Legalese contract could be compiled to multiple natural languages. Each version would be provably identical. This would be valuable in multilingual environments.
- A Legalese contract could be forward-compatible with the newfangled gewgaws coming down the pike, like Ethereum.
- Whenever you talk about semantics, ontologies come up. See Olog, LKIF, and FIBO
Modeling Social Practice
What if lawyers started working more like programmers?
- Opensource dynamics might lead to the development of reusable, public, clause libraries, published under an MIT, BSD, GPL, or CC license.
- Legal templates and precedents might end up on Github.
- End-users might bypass the priesthood of lawyers, and draft their own contracts.
- Corporate secretaries could go the way of the switchboard operator or tax preparer.
- Confidence in the codebase could arise from the bazaar model of contract development (“given enough eyeballs, all bugs are shallow”), from reputation systems, and other transparent, crowd-sourced mechanisms.
- As the richly interpretable saying goes, “Law is Code”. (MIT 1, MIT 2) and, conversely, Code is Law.
- Legislative and regulatory constraints may be modeled using a declarative language.
- Contracts and execution relations may be automatically produced as satisfactions of constraints.
- Oracle Policy Automation does this commercially. Carl Malamud and Thomas Bruce might argue that this should be done in an open way.
- Xcential’s LegisPro helps legislators get their words out in XML.
- An Empirical Approach to the Semantic Representation of Laws
- On Rule Extraction from Regulations
- The British Nationality Act as a Logic Program
- Logic Programming for Large Scale Applications in Law
- LREC2010 Workshop Proceedings
- Conferences include JURIX and JURIS Informatics
- JURIX 2016
- Artificial Intelligence for Justice
- ICAIL (IAAIL)
- FutureLaw 2014: Forging an Open Legal Document Ecosystem
- FutureLaw 2013: Computational Law and Contracts
- Harry Surden, Computable Contracts, 2011
- New Breakthroughs in Computational Law, 2013
- FutureLaw | The State of the Art of Legal Technology Circa 2015
- Hammurabi Project hosts its DSL in Wolfram Language (Mathematica). An earlier version developed a DSL called Akkadian.
- You've heard of XBRL, now the SEC wants Python.
- Also FpML
- Monitoring multi-party contracts for e-business, Lai Xu
- Formal Specification of Web Service Contracts for Automated Contracting and Monitoring
- A Contract Compliance Checker, Ioannis Sfyrakis shows an Event-Condition-Action language called EROP
- Eris:legal brings compatibility with smart contracts
Formal Verification of Smart Contracts
On the spectrum of software reliability, smart contracts ought to live near-mission-critical or life-critical software – cryptosystems, human-crewed spacecraft, hospital equipment. Today, they’re closer to enterprise web-apps.
The need for formal systems is dawning on r/ethereum:
- Can we please never again put 100m in a contract without formal correctness proofs?
- The bug which the “DAO hacker” exploited was not “merely in the DAO itself”
- Ethereum’s Solidity is also experimenting with formal verification.
- This list of languages with compile into the EVM
- Certified Symbolic Management of Financial Multi-party Contracts
- Safer smart contracts through type-driven development
- Evaluation of Logic-Based Smart Contracts for Blockchain Systems
- Validation and Verification of Smart Contracts: a Research Agenda. Daniele Magazzeni, Peter McBurney, William Nash. IEEE Computer Journal, Special Issue on Blockchain Technology for Finance. September 2017
- Formal Verification of Smart Contracts: Short Paper
Legalese wants to apply the same ideas to legacy-compatible contracts – even those that do not live on the blockchain.
The research continues, under the umbrella of projects like MIREL.
Built on all this research is the LegalTech Industry Today.