131–140 of 232 posts
Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B. Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.
I don't think this is obvious in python, at all. You are programming without thinking much about invariants and properties.
Earlier quoted context omitted.
> The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. The world is changing. In high-growth-potential areas, I think we're starting to see a shift away from the style of software where "what to build is hard but how to build is easier" and toward a…
> automated trading > It's really obvious what we want the system to do Nope.
>Nope.
Hedge funds and trading firms are some of the top donors to/supporters of the formal methods community. They sponsor conferences, hire tons of formal methods experts, buy products and services from formal methods startups, and develop/use formal methods internally.
So...
Yup.
(I do understand there's a substantive point being made, and I think my reply to the sibling comment by temporal addresses that point. So maybe that's the right place to continue discussion.)
Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B. Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.
I had a section on "high-availability software" that I cut due to not being able to research it thoroughly. For the most part cars and medical devices and stuff don't use FM because there's pretty much no oversight. Aircraft, though, are a super interesting case here. I'll be honest, I'd probably trust code that's gone through DO-178C more than I would trust code that's been formally verified. I _believe_ there's bee…
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:…
We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation), but we're making steady progress. One could reasonably expect having a verified, deployable implementation in 3-4 years if people continue working on it.
It remains to be seen whether people would switch to that from Core (very unlikely) or Core would adopt it as a component to replace its existing consensus code (interesting possibility, but also unlikely).
[1] - https://github.com/certichain/toychain
Earlier quoted context omitted.
Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project ex…
I think it's worse than that. I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program. I wasn't really confident afterwards that the "proved" software actually did work. I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quick…
So I actually had more confidence in the code than I did in the spec.
And I think this answers the question of the OP: people don't use formal methods because
(a) the vast majority of problems don't start out with a formal spec
(b) the gap between informal and formal is vastly more relevant than the one between different formalisms
(c) formal methods are significantly worse at bridging the formal/informal gap than most programming languages
And yes, when you have a sub-problem that is mostly formal, then it can make sense, particularly if there's a lot riding on it.
Earlier quoted context omitted.
think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations Every government IT project that is years late and billions over budget is because of this
False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.
If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…
For example an integer. In most languages and tools this is a primitive.
But most of the time we need a specific type of integer, for example a positive natural number. You can use a unsigned integer for this but that will include a zero wich we don't want.
So maybe you can use a type/domain object for this in your code, but what about the database field or communication methods?
It all can be done but with a lot of hussle.
I think it would help if we had more primitives that would work in the complete stack.
But then the question is: should ISO 639-2 also be a primitive?
Earlier quoted context omitted.
Proof in formal methods means the mathematical kind: with certainty the program / function implements the specification. Mathematicians can also prove something irrelevant or useless, or something fundamental like 1+1=2.
Well, yes, but if mathematicians prove something then we know it is true. And if they can't prove the trivialities, that would be a crisis for the entire discipline, because 1+1=2 relates to everything they do. If software people prove something we also know it is true, but not that it usefully relates to the software. In fact, 0.1+0.2 is likely != 0.3 for most software. You can prove you have integer types or fracti…
Proofs always rely on some sort of axiomatic system. Otherwise you don't have any basis for starting deductions. In most cases "the hardware conforms to its spec" can be considered a reasonable axiom (unless maybe in space flight where cosmic rays may cause appreciable amounts of random behavior).
If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…