Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well: it's very hard to do the formal verification.
Why Don't People Use Formal Methods?
41–50 of 232 posts
Re: Why Don't People Use Formal Methods?
#42Which universities teach formal methods?
- q=formal+verification https://www.class-central.com/search?q=formal+verification
- q=formal-methods https://www.class-central.com/search?q=formal+methods
Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
Is there a certification for formal methods? Something like for engineer-status in other industries?
What are some examples of tools and [OER] resources for teaching and learning formal methods?
- JsCoq
- Jupyter kernel for Coq + nbgrader
- "Inconsistencies, rolling back edits, and keeping track of the document's global state" https://github.com/jupyter/jupyter/issues/333 (jsCoq + hott [+ IJavascript Jupyter kernel], STLC: Simply-Typed Lambda Calculus)
- TDD tests that run FV tools on the spec and the implementation
What are some examples of open source tools for formal verification (that can be integrated with CI to verify the spec AND the implementation)?
What are some examples of formally-proven open source projects?
- "Quark : A Web Browser with a Formally Verified Kernel" (2012) (Coq, Haskell) http://goto.ucsd.edu/quark/
What are some examples of projects using narrow and strong AI to generate perfectly verified software from bad specs that make the customers and stakeholders happy?
From reading though comments here, people don't use formal methods because: cost-prohibitive, inflexibile, perceived as incompatible with agile / iterative methods that are more likely to keep customers who don't know what formal methods are happy, lack of industry-appropriate regulation, and cognitive burden of often-incompatible shorthand notations.
Re: Why Don't People Use Formal Methods?
#43I think the easy answer is: "because life isn't formal"
There is an intersection.
The places you might need defined and formal methods to make people happy and the places you might actually want to sling some code to make people happy? That intersection point?
Tiny
Re: Why Don't People Use Formal Methods?
#44I did an internship at a company building aviation hardware and software. Since everything was safety critical we used formal methods and things moved at a snail's pace. When verification becomes the most important thing everything changes. The design specification doesn't make sense? It will take months to get it changed, write whatever code you can convince someone verifies against the design. Compile times are lon…
Sounds like a good job.
Re: Why Don't People Use Formal Methods?
#45Part of the problem is that TLA+ syntax and tooling is horrendous. Creating something more modern and widely adoptable is a key for Mass scale applications.
Re: Why Don't People Use Formal Methods?
#46Earlier quoted context omitted.
Unlike the case of building an airplane, when you’re developing software you don’t know when you start sometimes if you want to build an airplane or a helicopter, or even if you want to fly, or indeed, if you’re building a vehicle of any kind, and not some kind of corn mill or a movie theater, perhaps.
The thing about software, indeed, most of it isn't space shuttles or life support systems. But it can go from paper airplanes to model airplanes to real airplanes more quickly than you'd think. Your hobby website could take-off to be an income and then a company and have leftover code all around.
It does usually go from paper airplanes, to model airplanes, to real airplanes. But if you set out to build a real airplane, you'd probably end up with a train.
Re: Why Don't People Use Formal Methods?
#47As a person who does and who's founded a company partially on the basis of the value of them, my opinion is that, in-part, it's because the ecosystem is extremely fractured, the tools are often an esoteric projection of the inside walls of one mad scientist's head turned into software, and they often don't scale very well (mostly due to the two previously mentioned conditions).
Additionally, the tools are often designed to empower a kind of pre-existing "priesthood" of a particular kind of verification practicioner, not necessarily to generally enable a more rigorous software development life-cycle by being approachable.
Granted we're trying to change a fair chunk of that, but that's sort of the status quo at the moment.
Lastly, there are some cultural forces in the software industry which aren't all that aligned or interested in making commonplace software development as rote, boring, and predictable as steel beam construction. But, I think those can eventually be overcome when people see the value of enabling a new bar for the sophistication of software innovations (e.g. like FEA and CFD did for mechanical systems).
Re: Why Don't People Use Formal Methods?
#48> This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the spec.
This seems to ignore a vast majority of possible software. It's easy to confirm/test whether a function, with no state, takes a certain input and produces a certain output. You can write that in a spec. You can unit test that. But that ignores the whole concept of state; the whole state of the system. If X happened yesterday, Y happens now, and X and Q are true, and it's a Wednesday and a full moon then the output is Z. By the time you've encoded that and every other variation into a spec, congratulations you've written the software!
Re: Why Don't People Use Formal Methods?
#49Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well:…
This is why currencies like Cardano were created.
Re: Why Don't People Use Formal Methods?
#50There is a lot of work done now with formal methods used for smart contract verification. MakerDAO formally verified correctness of their contracts last year: https://github.com/dapphub/k-dss/