3 ms·

As someone who hacks on code but doesn't have a true computer science or math background, I have a hard time even wrapping my head around what the hell "formal

As someone who hacks on code but doesn't have a true computer science or math background, I have a hard time even wrapping my head around what the hell "formal methods" are. How can you write proofs that a whole piece of software works? Especially since software is often compromised of tons of different libraries and frameworks etc. I could understand proving a certain piece, like a specific algorithm, but how are formal methods better than unit tests? I think my brain is just too small to understand. It feels to me, as a relative layman, like pablum.

andrewflnr 4y ago
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.
dwohnitmok 4y ago
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).
exdsq 4y ago
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-spec.pdf 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-verified-porn-browser-in-coq.html 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 https://galois.com
marcosdumay 4y ago
"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.
rstuart4133 4y ago
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.

andrewflnr 4y ago

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.

dwohnitmok 4y ago

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).

exdsq 4y ago

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-spec.pdf 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-verified-porn-browser-in-coq.html 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 https://galois.com

marcosdumay 4y ago

"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.

rstuart4133 4y ago

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.