Hacker News new | ask | show | jobs
by mengwong 3432 days ago
Contracts are similar to software in many ways, but a few crucial differences justify a whole new programming language custom-made for the task.

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)

1 comments

Incredibly valuable thoughts, Meng – thank you.