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 s

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.