Legalese - Rules Automation

"There is this tremendous body of knowledge in the world of academia where extraordinary numbers of incredibly thoughtful people have taken the time to examine on a really profound level the way we live our lives and who we are and what we've been. That brilliant learning sometimes gets trapped in academia and never sees the light of day." — Malcolm Gladwell

(at least) 70 years of legal informatics

The legal informatics industry is older than most web developers today.

An (incomplete) history in rough chronology—let us know if we missed something.

Formalising Contracts

The urge to formalize goes back at least as far as Leibniz, that's the early 18th century
Lee Loevinger's Jurimetrics -- The Next Step Forward, 1948: "apparently, it has never occurred to the professional disciples of the subject that the trouble with law is not the public but the lawyers, that what is needed is not publicity but progress"
Layman E. Allen in 1956, Symbolic Logic: A Razor-Edged Tool for Drafting and Interpreting Legal Documents
Computer Science and Law, 1980 where every chapter seems to have become the underpin of at least one legaltech startup
Some Speculation About Artificial Intelligence and Legal Reasoning by Bruce G Buchanan & Thomas E Headrick in 1970
In the 1980s, the British Nationality Act was encoded in Prolog
The Role of Common Ontology in Achieving Sharable, Reusable Knowledge Bases by Thomas R Gruber in 1991
The Artificial Intelligence and Law Journal was founded in 1992
Isomorphism and legal knowledge based systems by TJM Bench-Capon & F P Coenen in 1992
Attempto Controlled English is an example of a formal/natural hybrid language which could be a compiler target, and has been under development since 1995
Executable English
Nick Szabo, Smart Contracts, 1997
The Representation of Legal Contracts by Daskalopulu & Sergot, 1997
Composing Contracts: An Adventure in Financial Engineering, 2000 by Simon Peyton Jones, Jean Marc-Eber, and Julian Seward
Nick Szabo on A Formal Language for Analysing Contracts, a preliminary draft from 2002
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; the RFP was issued in 2003, and v.1.0 of the formal specification was released in 2008
The Ricardian Contract, 2004 relates legal language with executable code via parameterization
The RuleML Initiative has been collaborating with OASIS on Legal XML, Policy RuleML, LegalRuleML, and related efforts since 2004; see Modelling Contracts Using RuleML
Structured Products and Time Travel, 2004 reviews potential solutions for overcoming the challenges of valuing structured products on past, present, and future dates
Using the Event Calculus for Tracking the Normative State of Contracts by Andrew D. H. Farrell, Mark J. Sergot, Mathias Sallé, Claudio Bartolini, 2005
Structuring, Pricing, and Processing Complex Financial Products with MLFi, 2005 described MLFi concepts and applications
ContractLog: An Approach to Rule Based Monitoring and Execution of Service Level Agreements by Adrian Paschke, Martin Bichler, and Jens Dietrich, 2005
Realization of Natural Language Interfaces Using Lazy Functional Programming by RA Frost, 2006
Towards a Formal Language for Electronic Contracts, 2007 describes CL
Abstract Specification of Legal Contracts, Prisacariu & Schneider, 2009
Challenges in the Specification of Full Contracts, GJ Pace and G Schneider, 2009
Need for a Common Language for All Securities and Financial Contracts, 2010 by the National Research Council
A Software Tool for Legal Drafting by Daniel Gorin, Sergio Mera, and Fernando Schapachnik, 2011
Formal Methods as a Link between Software Code and Legal Rules by Daniel Le Métaye, 2011
Contract Formalisation and Modular Implementation of Domain-Specific Languages, Tom Hvitved's 2012 PhD Thesis (the first chapter offers a comprehensive survey of prior art in contract formalisation)
Harry Surden on Computable Contracts, 2012
Towards a common financial language, 2012 speech by Andrew Haldane, Executive Director (Financial Stability) of the Bank of England
A toolkit for model checking contracts using SPIN / Promela rather than Uppaal by Abubkr Abdelsadiq at Newcastle, 2013
The REMU project has supported research at the Department of Computer Science at Chalmers University of Technology and the University of Gothenburg, 2013–2017
These Are Your Rights: A Natural Language Processing Approach to Automated RDF Licenses Generation by E Cabrio, 2014
Automated Decision Support for Financial Regulatory/Policy Compliance, using Textual Rulelog, 2014
Stanford University's Computable Contracts Initiative started in 2015
Next Generation Contracts by Helena Haapio, 2015
Contracts as Automaton: The Computational Representation of Financial Agreements, Floyd & Goodenough (first published 2015 then revised in 2017)
Analysing Normative Contracts by John J. Camilleri, 2015
Smart Contract Templates by Christopher D. Clack, Vikram A. Bakshi, and Lee Braine, 2016
Bridging the gap between expectation and reality compares smart vs traditional contracts, 2016
Logic in the Theory and Practice of Lawmaking, 2016
DMN: Decision Model and Notation Specification, v1.1 was published in June 2016
Joe Dewey's essay on ContractCode, 2016
Toward Machine-Understandable Contracts, 2016 by Stanford's Computable Contracts initiative
Stephen Wolfram's blogpost on Computational Law, Symbolic Discourse and the AI Constitution, October 2016
2016 Nobel Prize in Economics awarded to Oliver Hart and Bengt Holmström for their work in Contract Theory
Contracts and Computation — Formal modelling & analysis for normative natural language by John J. Camilleri, 2017
Kowalski & Sadri's Logic Production Systems relates two dual models of computation, commercialized as Logical Contracts, 2018

Formalising Regulations

As the richly interpretable saying goes, "Law is Code" and, conversely, Code is Law (Lessig, 2000). Legislative and regulatory constraints may be modeled using a declarative language.

In 1986, Martin Sergot et al explored The British Nationality Act as a Logic Program
Logic Programming for Large Scale Applications in Law, 1987
The Treatment of Negation in Logic Programs for Representing Legislation by Robert Kowalski, 1989
Since 1988, JURIX has held annual conferences on legal knowledge and information systems
Towards Regulatory Compliance: Extracting Rights and Obligations, 2006
Digitising the World's Laws, Claire M. Germain, 2010
On Rule Extraction from Regulations, 2011
An Empirical Approach to the Semantic Representation of Laws, 2012
New Breakthroughs in Computational Law, 2013
Xcential's LegisPro helps legislators get their words out in XML
FormaLex published about formalising the Argentinean Customer Protection Act in 2017
The Hammurabi Project hosts its DSL in Wolfram Language

Modelling Performance

Monitoring multi-party contracts for e-business by Lai Xu, 2004
Formal Specification of Web Service Contracts for Automated Contracting and Monitoring, 2007
A Contract Compliance Checker by Ioannis Sfyrakis, 2012

Formal Verification of Smart Contracts

Formal methods and languages like Agda, Idris, Why3, and CoQ, not to mention specification languages like Z, hold much promise. 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.

See The Atlantic on why formal verification is important.

The need for formal systems appears to be dawning on r/ethereum:

Key Papers:

Startups: Adjoint, Kadena (PACT), Tezos, Cardano

Academia-Industry Partnerships

Harvard's Berkman Klein Centre for Internet & Society
Law.MIT.edu
Stanford's Computational Law and CodeX Center for Legal Informatics
The Legal Informatics Research Network
Law OS at the Santa Fe Institute
The Law Lab at Illinois Tech
The Accord Project
University of Oslo's Norwegian Research Center for Computers and Law

Workshops & Conferences

International Conferences on AI & Law (ICAIL) since 1987
JURIX since 1988
CodeX FutureLaw Conference since 2013
AI4J (Artificial Intelligence for Justice)
Legal Geek Conference in London
MIT Legal Forum
Singapore's TechLaw.Fest

"Well, all information looks like noise until you break the code" — Hiro Protagonist, Snow Crash (Neal Stephenson, 1992)

This is Part II of our series on Why Computational Law. See Part I: The Problem with Legal and Part III: Computational Law.

Why Computational Law, Part II: 70 Years of Legal Informatics