4 ms·

Formal methods is what happens when you try to do engineering in the traditional sense in the software space. You sit down, design, find a specification, and th

by voxl 3y ago

Formal methods is what happens when you try to do engineering in the traditional sense in the software space. You sit down, design, find a specification, and then build to spec. It's arguably an idealized version, even, because depending on the methods you cannot fail the spec if you succeed in building it. Only a small group of software engineers are interested in this principled approach. Hell many software engineers are scared of recursion.

sabas123 3y ago
You can also write a formal spec based on a reference. But it will be harder then doing it up front most likely.
seeknotfind 3y ago
It's not just that they are afraid. No one has succeeded in building production-level systems at scale purely using "formal methods". There are a variety of ways to measure how a system compares to a spec. For instance, you can measure throughput at various points in a system. However, formal methods are much more detailed, and when they are applied today, it's usually within a limited context as a way to verify or do model checking.
- colordrops 3y ago
  Right, the tradeoff in time/resources for doing upfront formal verification vs fixing bugs after they are found is almost never worth it. Formal verification isn't even used for most aerospace software.
quatrefoil 3y ago
That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. For a bridge, you specify that it needs to withstand specific static and dynamic loads, plus several other things like that. Once you have the a handful of formulas sorted out, you can design thousands of bridges the same way; most of the implementation details, such as which color they paint it, don't matter much. I'm not talking out of my butt: I had a car bridge built and still have all the engineering plans. There's a lot of knowledge that goes into making them, but the resulting specification is surprisingly small. Now try to formally specify a browser. The complexity of the specification will probably rival the complexity of implementation itself. You can break it into small state machines and work with that, but if you prove the correctness of 10,000 state machines, what did you actually prove about the big picture? If you want to eliminate security issues, what does it even mean that a browser is secure? It runs code from the internet. It reads and writes files. I talks directly to hardware. We have some intuitive sense of what it's supposed and not supposed to do, but now write this down as math...
- pydry 3y ago
  My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too. I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.
  - AnimalMuppet 3y ago
    First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
    - NovemberWhiskey 3y ago
      >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
      - pfdietz 3y ago
        Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
asplake 3y ago
There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. On the flip side, type systems bring at least some sense of proof into programming.
- NovemberWhiskey 3y ago
  >If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. That seems like a weird conclusion to me. You definitely can't write a "correct" program unless you know what you expect it to do. It's easier to write a specification than a program, because a specification is at a higher level of semantic abstraction.
  - AnimalMuppet 3y ago
    You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
    - NovemberWhiskey 3y ago
      I don't think I did dodge the question. Is it easier to write a correct specification that correct code? Yes, absolutely, because in a specification I can specify outcomes without having to say how they're achieved, and I can specify results that are invariant over time without having to say how they're maintained, etc. A specification is essentially a bridge between, on the one hand, a higher-level requirements document that's probably imprecise and/or contradictory and/or incomplete and, on the other, code that has to be completely deterministic.
      - staunton 3y ago
        I agree with you but still want to play devil's advocate regarding you argument: > [It's easier to write specifications than implementations because] in a specification I can specify outcomes without having to say how they're achieved It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. This way, "correct" isn't a meaningful category, there's only "incorrect in retrospect". This is how most software is made and for most applications I would expect cost-benefit analysis to favor it.
odyssey7 3y ago
Application-level software engineering hasn't been about hand-writing for-loops for a long time, but there's a tendency for people to feel self-satisfied in what's familiar and what they worked hard to master. Now that LLMs can write for-loops, too, I've hoped that the field will reconsider the activities that it considers to be valuable. The essential complexity is more about what you described: sit down, design, find a specification. The build to spec part, in the 21st century, can be a tooling step that takes the spec as input. Perhaps the next step for the industry's state of the art in application-level software engineering is mastering formal spec languages, to seriously tailor the scope of work to the essential complexity of mediating between the agile world of human requirements and the formal world of computing systems. But I won't hold my breath--society is inured to software bugs as a fact of life, and programmers are used to being paid to endlessly patch their own mistakes.
- knome 3y ago
  >can be a tooling step that takes the spec as input It's been said that a sufficiently detailed spec already has a name: a program.
  - odyssey7 3y ago
    Sure, but that's just wordplay. There are genuine, meaningful differences between technologies. Professionals should be able to weigh and consider them in various contexts.
  - someplaceguy 3y ago
    > It's been said that a sufficiently detailed spec already has a name: a program. You could create a spec that would specify exactly what a program does, but generally speaking that would have no useful purpose. For every program that does something, there are multiple ways to implement it. Often, different ways of implementing a program have different performance profiles, which is why many programs become more complex than the most naive way of implementing it. A spec almost never specifies anything other than the simplest possible way that a program should be implemented (because when creating a spec, performance is irrelevant). This is usually way easier to make sure that it is correct than a spec that would specify exactly how a program should be implemented, including things done for performance. Furthermore, you don't have to necessarily trust a specification. Specs can also be proven to have certain properties, i.e. they can be formally verified and proven to have absence of (perhaps certain classes of) bugs, and in some cases, can even be proved to have full correctness (yes, the spec itself, not just the program that implements it). So I don't think it's fair to equate a program to a "sufficiently detailed spec", since most of those details are actually irrelevant (or at least, they should be, and can be proven to be) with regards to the correctness of a program.
pphysch 3y ago
> Only a small group of software engineers are interested in this principled approach. Only a small fraction of software applications can be specified up-front. Most software is enterprise software, entertainment software, etc.; software that evolves, where a priori 100% specification is a fool's errand.
- thfuran 3y ago
  That the spec can change over time just means you'll change the spec, not that you shouldn't or can't have one.
  - pphysch 3y ago
    In practice, software development methodologies that rely heavily on a complete spec (formal verification, 100% test coverage, pure programming, etc) do not perform well when the spec changes underneath them. It's doable but requires enormous resources and is almost never economical unless you're NASA.
GuB-42 3y ago
Traditional engineering is a lot messier than you make it look. Things are out of specs all the time, and engineers have to deal with that all the time. It is even worse because while you can prove a program mathematically correct, reality only has a passing interest in mathematical correctness.

by voxl 3y ago

sabas123 3y ago

You can also write a formal spec based on a reference. But it will be harder then doing it up front most likely.

seeknotfind 3y ago

It's not just that they are afraid. No one has succeeded in building production-level systems at scale purely using "formal methods". There are a variety of ways to measure how a system compares to a spec. For instance, you can measure throughput at various points in a system. However, formal methods are much more detailed, and when they are applied today, it's usually within a limited context as a way to verify or do model checking.

colordrops 3y ago
Right, the tradeoff in time/resources for doing upfront formal verification vs fixing bugs after they are found is almost never worth it. Formal verification isn't even used for most aerospace software.

quatrefoil 3y ago

That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. For a bridge, you specify that it needs to withstand specific static and dynamic loads, plus several other things like that. Once you have the a handful of formulas sorted out, you can design thousands of bridges the same way; most of the implementation details, such as which color they paint it, don't matter much. I'm not talking out of my butt: I had a car bridge built and still have all the engineering plans. There's a lot of knowledge that goes into making them, but the resulting specification is surprisingly small. Now try to formally specify a browser. The complexity of the specification will probably rival the complexity of implementation itself. You can break it into small state machines and work with that, but if you prove the correctness of 10,000 state machines, what did you actually prove about the big picture? If you want to eliminate security issues, what does it even mean that a browser is secure? It runs code from the internet. It reads and writes files. I talks directly to hardware. We have some intuitive sense of what it's supposed and not supposed to do, but now write this down as math...

pydry 3y ago
My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too. I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.
- AnimalMuppet 3y ago
  First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
  - NovemberWhiskey 3y ago
    >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
    - pfdietz 3y ago
      Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.

asplake 3y ago

There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. On the flip side, type systems bring at least some sense of proof into programming.

NovemberWhiskey 3y ago
>If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. That seems like a weird conclusion to me. You definitely can't write a "correct" program unless you know what you expect it to do. It's easier to write a specification than a program, because a specification is at a higher level of semantic abstraction.
- AnimalMuppet 3y ago
  You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
  - NovemberWhiskey 3y ago
    I don't think I did dodge the question. Is it easier to write a correct specification that correct code? Yes, absolutely, because in a specification I can specify outcomes without having to say how they're achieved, and I can specify results that are invariant over time without having to say how they're maintained, etc. A specification is essentially a bridge between, on the one hand, a higher-level requirements document that's probably imprecise and/or contradictory and/or incomplete and, on the other, code that has to be completely deterministic.
    - staunton 3y ago
      I agree with you but still want to play devil's advocate regarding you argument: > [It's easier to write specifications than implementations because] in a specification I can specify outcomes without having to say how they're achieved It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. This way, "correct" isn't a meaningful category, there's only "incorrect in retrospect". This is how most software is made and for most applications I would expect cost-benefit analysis to favor it.

odyssey7 3y ago

Application-level software engineering hasn't been about hand-writing for-loops for a long time, but there's a tendency for people to feel self-satisfied in what's familiar and what they worked hard to master. Now that LLMs can write for-loops, too, I've hoped that the field will reconsider the activities that it considers to be valuable. The essential complexity is more about what you described: sit down, design, find a specification. The build to spec part, in the 21st century, can be a tooling step that takes the spec as input. Perhaps the next step for the industry's state of the art in application-level software engineering is mastering formal spec languages, to seriously tailor the scope of work to the essential complexity of mediating between the agile world of human requirements and the formal world of computing systems. But I won't hold my breath--society is inured to software bugs as a fact of life, and programmers are used to being paid to endlessly patch their own mistakes.

knome 3y ago
>can be a tooling step that takes the spec as input It's been said that a sufficiently detailed spec already has a name: a program.
- odyssey7 3y ago
  Sure, but that's just wordplay. There are genuine, meaningful differences between technologies. Professionals should be able to weigh and consider them in various contexts.
- someplaceguy 3y ago
  > It's been said that a sufficiently detailed spec already has a name: a program. You could create a spec that would specify exactly what a program does, but generally speaking that would have no useful purpose. For every program that does something, there are multiple ways to implement it. Often, different ways of implementing a program have different performance profiles, which is why many programs become more complex than the most naive way of implementing it. A spec almost never specifies anything other than the simplest possible way that a program should be implemented (because when creating a spec, performance is irrelevant). This is usually way easier to make sure that it is correct than a spec that would specify exactly how a program should be implemented, including things done for performance. Furthermore, you don't have to necessarily trust a specification. Specs can also be proven to have certain properties, i.e. they can be formally verified and proven to have absence of (perhaps certain classes of) bugs, and in some cases, can even be proved to have full correctness (yes, the spec itself, not just the program that implements it). So I don't think it's fair to equate a program to a "sufficiently detailed spec", since most of those details are actually irrelevant (or at least, they should be, and can be proven to be) with regards to the correctness of a program.

pphysch 3y ago

> Only a small group of software engineers are interested in this principled approach. Only a small fraction of software applications can be specified up-front. Most software is enterprise software, entertainment software, etc.; software that evolves, where a priori 100% specification is a fool's errand.

thfuran 3y ago
That the spec can change over time just means you'll change the spec, not that you shouldn't or can't have one.
- pphysch 3y ago
  In practice, software development methodologies that rely heavily on a complete spec (formal verification, 100% test coverage, pure programming, etc) do not perform well when the spec changes underneath them. It's doable but requires enormous resources and is almost never economical unless you're NASA.

GuB-42 3y ago

Traditional engineering is a lot messier than you make it look. Things are out of specs all the time, and engineers have to deal with that all the time. It is even worse because while you can prove a program mathematically correct, reality only has a passing interest in mathematical correctness.