Thirty Years of Legal Informatics

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

Everything “THEDAO” tried to be, it could have been correctly and in full compliance with the law. For this reason, what blockchain companies should be trying to do is take complex financial, business, and governance processes and turn them into machine-readable protocols that also tick all of the human requirements, legal or otherwise. A bit of code that does all those things is what a smart contract actually is.

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.

Formalizing Contracts

Other efforts

Formalizing Law

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.

Modeling Entities

  1. 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.
  2. 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.
  3. Alternatively, these changes can be modeled with a bitemporal database—ACID CRUD. Either way, formal structure can apply.
  4. 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)

  1. Automated legal reasoning is a hard problem. Corp sec is possibly the easiest practical domain of application.
  2. 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.
  3. 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.
  4. 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.
  5. A particular document may be a collection of resolutions, or a contract.

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.

  1. Natural-language contracts often look like somebody trying to program without knowing any programming languages.
  2. 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.
  3. Few contracts use basic structured programming idioms. Most complex contracts read like spaghetti codeobject/machine code whose control flow jumps all over the place, from one clause reference to another.
  4. Some contracts are (inadvertently or deliberately) obfuscated.
  5. Imprecisions abound. Bugs result.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. A Legalese contract could be compiled to multiple natural languages. Each version would be provably identical. This would be valuable in multilingual environments.
  11. A Legalese contract could be forward-compatible with the newfangled gewgaws coming down the pike, like Ethereum.
  12. Whenever you talk about semantics, ontologies come up. See Olog, LKIF, and FIBO

Modeling Social Practice

What if lawyers started working more like programmers?

Software engineering teams often need to integrate new team members, fix bugs, and refactor existing code, which are all tasks that require a deep understanding of code written by others who are often no longer available to provide support or clarification. These requirements suggest that the tools used by software engineers to track progress, monitor potential vulnerabilities, or simply gain an understanding of an existing software codebase may be useful for serving the same functions when applied to legal code.
  1. Opensource dynamics might lead to the development of reusable, public, clause libraries, published under an MIT, BSD, GPL, or CC license.
  2. Legal templates and precedents might end up on Github.
  3. End-users might bypass the priesthood of lawyers, and draft their own contracts.
  4. Corporate secretaries could go the way of the switchboard operator or tax preparer.
  5. 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.

See Also

Modeling Regulations

  1. As the richly interpretable saying goes, “Law is Code”. (MIT 1, MIT 2) and, conversely, Code is Law.
  2. Legislative and regulatory constraints may be modeled using a declarative language.
  3. Contracts and execution relations may be automatically produced as satisfactions of constraints.
  4. Oracle Policy Automation does this commercially. Carl Malamud and Thomas Bruce might argue that this should be done in an open way.
  5. Xcential’s LegisPro helps legislators get their words out in XML.

Modeling Performance

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.

The need for formal systems is dawning on r/ethereum:

Papers include:

Startups include:

Legalese wants to apply the same ideas to legacy-compatible contracts – even those that do not live on the blockchain.

Now what?

The research continues, under the umbrella of projects like MIREL.

Built on all this research is the LegalTech Industry Today.