Utterly Unpersuasive: Formal Methods and Law (2019)

"The point of most cryptography and security features is to use math to represent and symbolically transfer liability and risk between transaction counterparties"

What is the liability here? For example, the company holds different level of liability in a data breach, depending on whether they implement the security correctly - is that what you mean?

Exactly this. The Platonic ideal of statutory interpretation is the “no vehicles in the park” statute. It’s simple enough on the surface but you can think of an infinite number of edge cases that demand nuance (e.g. Scooters? A war memorial featuring a tank? A wheelchair?).

Enumerating and handling these cases in a formal mathematical sense is at best futile and at worst leads to absurd outcomes. Law isn’t made formally because lawyers don’t know how, it’s because intelligently applied common sense is an essential part of a sane legal system. [0]

[0] For what it’s worth, it’s not as if the formalism vs. common sense debate is actually settled in the legal sphere. See, e.g., the debate about textualism vs. legislative intent in American statutory interpretation. Even the textualist position lies much, much further along the spectrum than formal specification though, and it has its own problems.

Powerful interests?

Even an informal process like TDD is a huge improvement in this space. You can’t write tests first without an at least implicit specification.

It is really wonderful though when the algorithm just falls out of the specification. Dijkstra’s derivation of smoothsort[1] is a nice example.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD07xx/E...

You correctly understand the difficulty. AFAICT formal methods only really work in relatively small, self-contained scenarios. You wouldn't want to attempt a formal proof of a Python web app. The seL4 microkernel is one of the biggest verified projects I know of. Maybe reading about that would give you an idea of how things get put together in the field.

Formal methods in a nutshell are using code to statically analyze and prove things about code. The reason this has value despite sounding circular is that often times the code we use to write the statements we wish to prove is easier to understand than the code we are proving.

It is fundamentally the reason why tests are useful, despite also being code. Even though tests themselves may contain bugs, they are still useful because they are simpler and easier to understand than the code being tested.

> how are formal methods better than unit tests?

Strictly speaking, unit tests are a kind of formal method. They are after all code being used to test code. Other formal methods tend to try to concern themselves with universal statements rather than one-off examples as unit tests do. E.g. proving that a program will never crash no matter what input is given to it (whereas a unit test would prove that a program will not crash for a single given input).

I worked on a blockchain that used formal methods as part of the development workflow. The development process was essentially writing a paper that formalised an algorithm or a protocol, an implementation in Agda that would generate Haskell (or written straight in Haskell), property based tests against the paper, and then a whole business analysis/QA side where there'd be a requirements matrix against the paper with unit/integration/end-to-end tests on the features too. So you'd end up with formally checked code, property based tests, unit tests, integration tests, end to end tests, manual checks, and a few other tools too. This was a pretty slow process but on the two major product releases I worked on, I can only remember one bug slipping through and that was patched before people realised (and not a major issue either). So I think this style of development can work if you can 1) afford it, 2) afford the time to do it, and 3) formulate the requirements in such detail upfront.

Here's an example of a formal method paper that explains how a specific protocol works: https://hydra.iohk.io/build/13099985/download/1/blockchain-s...

This is a fun example of doing something similar with Coq to build a porn browser: http://www.michaelburge.us/2017/08/25/writing-a-formally-ver...

And there are a couple companies out there that do this style of development as a consultancy - it's probably the closest to 'engineering' that software development can get (in my eyes) https://galois.com

"Formal methods" are anything a computer is able to do. (Things were originally defined the other way around, but if you have experience programing, that direction is more intuitive.)

You can prove that a piece of code is "correct" as long as you have a formal description of what it must do. That idea is quite useless for any code that people touch, because a formal description is about the same as a full program. But there are plenty of niches, like optimization, where you can just say "this program must do the same as this other program on any condition" where you have a simple formal description of correctness, that a computer can take and do the analysis for you.

Formal methods have been a holy grail for the decades I've been programming. Back in the day, they were utterly useless. If you define the goal as producing software that is guaranteed to fulfil it's requirements, they are still are hopelessly distant from achieving that goal. It's just too hard to formally prove everything.

However, we are making progress. Strongly typed systems are formal proofs your code adherers to some invariants. Compared to traditional format proofs (which largely consist of long complex mathematical statements about preconditions, post conditions, and invariants) they are delightfully simple and low overhead. It used to be that your strongly type system guaranteed you little more than you the arguments you passed matched what the method was expecting. But now Rust's type system gives you strong memory guarantees - there shall be no dangling points in Rust, and no two threads shall stomp over each others working memory. To me, this is am amazing advance. I never expected to see it in my lifetime.

Strong static type systems are the formal methods programmers actually use today. They are getting stronger, proving more and more. They are so good now they are invading areas that used to dismiss them as useless overhead - like Javascript with Typescript, and Python's and PHP's type annotations.

I'd be stunned (and almost certainly dead at the time) if formal systems ever got to the point proved a program exactly met it's requirements. Strong type systems don't try to prove that. But they do go a long way toward proving a program is internally consistent, but which I mean you don't add an float to a pointer, you don't access memory in an undefined state, and you don't have resource leaks. The end result is, as a Rust programmer will tell you, once you get the thing to compile (which can be a major hurdle) there is a good chance it will work.

For all the criticism crypto attracts here HN, it looks to be the area that will lead this drive. You see headlines about the costs of crypto bugs every week at least - because they exceed $10M. For every $10M bug, there must be hundreds that "only" lose a few $100k that we never hear about. The pressure to get it right the on the first release is immense.

Interestingly, and it seems completely lost on most HN commentators is crypto is at it's heart about building a world where all laws are written in software, assertions and promises the laws operate on aren't on paper and memories but rather can only be recorded in a blockchain, the judges are VM's executing code, and the jails have been replaced loss of crypto currency. The original article was about introducing formal methods to our existing law. I'd lay long odds this other mob, who is trying to replace out existing law with something else entirely, will beat them at delivering formally proved contracts between parties.

But unlike computer security, laws are not determined by hardware that never complain about exploitation. Law is operated by humans, and people may reject exploration by arguing the contract differently. Lawyers are trained to dispute humans rather than rules.