8 ms·

I don't understand why the author is so suspicious of formal methods. Other engineering disciplines are based on the application of solid, well-understood princ

by jolux 9y ago

I don't understand why the author is so suspicious of formal methods. Other engineering disciplines are based on the application of solid, well-understood principles from the natural sciences to practical problem domains. There are few solid, well-understood principles in computer science that are directly and obviously applicable to software engineering so far. I vigorously contest the idea that software engineering cannot be rigorous and so shouldn't try.

sillysaurus3 9y ago
Because there are what, six types of bridges? (EDIT: 36 according to wikipedia.) There are six thousand types of programs (as a wild guess), and they all interact with each other in an exponential explosion of complexity. For a formal method to work, it has to be generally applicable across a wide range of situations. There are methods like that in software engineering, and you see them in situations where the program is potentially life-threatening. But most programs would be hindered by this rigor.
- rubidium 9y ago
  Six types of bridges... Were you serious? There are definitely ways to apply formal engineering methods to software that greatly help its development. Computer programming is not a special snowflake. It's a field that (in many areas) refuses to grow up.
  - sillysaurus3 9y ago
    Forcing it to grow up would harm it, though. The engineers would move to companies that don't force those kinds of constraints. It's important to keep in mind what "growing up" translates to: slowing down. This has both economic and competitive implications. Sometimes it might be a win, but the vast majority of the time your ability to move quickly (and yes, occasionally break things) is an advantage.
    - lilott8 9y ago
      Yes and no. It is a natural progression of the industry. Those who cannot do "formal engineering" probably don't belong in engineering roles. Engineering, in general, imho, can be distilled down to this: Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints. If someone as an SE cannot do that, they really have no business being anywhere near any field of engineering.
      - pitay 9y ago
        Depends on the constraints you want to prove that the program will uphold. Some constraints may be impossible to prove, especially in non-real time contexts. For example, a program must run on a platform that doesn't have everything formally defined or have guarantees. If a program relies on that platform and that influences the program in a way that makes the constraint reliant on the platform, then you are out of luck. Another issue is choosing the constraints that the program will operate under. You would hope that the clients would give you the requirements including the constraints the software must operate under. But this isn't often the case. Having an incremental approach which includes clarifying requirements by mapping what the clients need to do to get their work done, which includes recording the specific steps that they perform or need to perform works pretty well when clients don't provide the requirements or constraints upfront. I am relatively ignorant on formal engineering, but I do like that you have provided a fairly clear definition, which was "Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints". It is better than the people saying know more math, without saying how, or what, or why it is useful in any clear way, and saying software is math just doesn't cut it.
        lilott8 9y ago
        That is a great counter example. I expect there to be a slow migration to platforms like [this formally verified microkernel](https://sel4.systems/ https://sel4.systems/). This will take time and a tremendous amount of effort. But will ultimately address the counter example. In the conclusion of this migration, this puts the SE field into line with the rest of engineering. Choosing the constraints for a project is no different in the context of CS than the context of any other fields -- electrical, mechanical, etc. It is a conversation, as you stated. This helps in many ways: it helps the developer understand exactly what the client wants, helps the client understand exactly what they are going to get, and helps build an implicit timeline replete with discrete and obvious deliverables and (if done correctly) those deliverables are fairly modular. Thanks! I, too, get frustrated that people just say 'math! math! math!' That isn't helpful or meaningful. This is a conclusion I came to after talking to quite a few of my friends and colleagues in different engineering disciplines.
  - pvg 9y ago
    It is a special snowflake because the semantics and correctness of nontrivial programs are often in the eye of the beholder (is Microsoft Word or Google Search 'correct'?). This isn't the case for bridges, cars or toasters. It's not just a matter of adding magic engineering dust until programming is engineering.
    - Denzel 9y ago
      No, the correctness is in the eye of a spec. Now, whether companies formally define their specs is a different story. Many startups don't. With that said, if Microsoft Word meets the given spec, then it's correct. One way to prove this correctness is with testing. This is the case for bridges as well. If I hand a spec to an engineering firm requesting a bridge from A to B at any given price. Well then, there's a lot of bridges that satisfy those constraints. Just because many software companies today don't choose to formally specify a spec and prove a programs correctness upon delivery doesn't mean it's a special snowflake. It just means those teams are immature. Sometimes software development doesn't require a mature team. Like most decisions, there's a cost and timing tradeoff.
      - stale2002 9y ago
        The problem with this line of thinking is that the problems that matter are not related to 100% implementing the spec correctly. The problems that matter are in the design of the spec to begin with. The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly. And do you know what the best way is to test whether you got the spec right? You deploy and see if the feature gets traction. The "spec" that matters is the success of the business. And building a product, and releasing it, is the way to formally test if your feature is "correct" according to the spec that is The Market.
        jolux 9y ago
        >The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly. It's both, though. You also can't tell if you've implemented them correctly if you don't have a formal spec.
  - deleted 9y ago
    [deleted]
  - mpweiher 9y ago
    Actually, it is fundamentally different in that just building the thing / just running the experiment is cheaper than doing the simulations or proofs. Every other discipline does simulations because actually running the experiment is magnitudes more expensive and time consuming. See "Why software development is an engineering discipline" https://www.youtube.com/watch?v=zDEpeWQHtFU
    - TeMPOraL 9y ago
      I agree. The primary thing distinguishing software development from other engineering fields is that the cost of building the product is essentially zero. Because building is what your compiler does. What a programmer does is design, and that is always influenced by the constraints of manufacturing - which, for software, are almost non-existent.
- jolux 9y ago
  I'll put it this way. In mathematics, the atomic unit of progress is the proof. Proofs are constructed from axioms and other, smaller proofs. The Curry-Howard correspondence is the direct correspondence between computer programs and mathematical proofs. When programming in a well-typed language, everything we do is a degenerate proof of something. I think it's entirely reasonable to try and make it easier to make less degenerate proofs, and encourage the re-centering of proofs as the atomic unit in programming, because they are for programming (as in math) a well-defined, solid formal system that solid systems can be built on in a way that nothing else can be in software, at least thus far. In a world where software flows more freely than water, the correctness and reliability of software systems must be taken with utmost seriousness. This applies to basically any tool that contacts end users, and a lot of ones that don't as well. What do you propose as the theoretical basis for the engineering science of software development?
  - sillysaurus3 9y ago
    I think it's self-evident that there is no theoretical basis for software development in the way that would satisfy your criteria. Software dev is generally a scattershot haphazard endeavor that involves trying dozens of angles until one of them works. That's an unsatisfying answer, but if we try to hide from the implications just because we don't like it, we'll end up creating companies that fail to startups without these constraints. It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter.
    - jolux 9y ago
      >I think it's self-evident that there is no theoretical basis for software development in the way that would satisfy your criteria. I don't think this is self-evident whatsoever. One of the problems in software engineering is that we never know when a solution is "right," we only know when it's vaguely not-wrong, and even then almost everything we create is still subtly wrong in a way we forgot to think about. Math is solid because there is certainty in the correctness of certain proofs, and these can be used as building blocks for further results. Philosophically speaking this is the closest we're going to get to "real" engineering practice in software, and we're pretty dang far from it if you know what that looks like. >Software dev is generally a scattershot haphazard endeavor that involves trying dozens of angles until one of them works. But this is a symptom of any pre-scientific field in engineering, it's not specifically endemic to software engineering. The main difference is that in software engineering we're applying math directly, and in other engineering fields we're applying science. In a certain sense, the natural sciences are purely empirical (modulo advanced physics of course, which overlaps with pure math and philosophy these days) while math and consequently computer science are purely rational. So, what are the solid elements in math? Proofs. Proofs are also how you ensure that the field actually moves forward and you're not stuck recreating solid results that already exist. Sound familiar? It happens constantly in software, but imperative and poorly-typed languages inhibit composability and reuse because they lend themselves easily to extremely specific solutions to general problems. >It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter. This is preposterous. Just because lives are not in danger does not mean that it's not worth doing right by the solution, and frankly I think a lot more lives are waiting to be put in danger by crappy software with bad security than you realize. It's already become almost dogma that all software engineers need to have a deep understanding of security, and I don't understand why correctness can't fall under that rubric as well. If we're going to be having Geohot or even Google or whoever building self-driving cars for possibly billions of people, enormous critical infrastructure projects coming under computer control, etc, the whole industry from education on up is going to have to have a serious attitude adjustment to keep up with the demands of safety, security, and reliability. It might not matter 99% of the time, (I think it's a lot more than that of course) but we need to make sure that we can as a discipline deliver that 1% when it is absolutely critical, and as of right now it doesn't seem like we can.
- KirinDave 9y ago
  So like, for example, Monads. Monads are applicable across every program ever written and with some rules laid out around them have remarkable properties. Comonads too. Can we use those? By your criteria, I mean.
- nautilus12 9y ago
  There may be thousands of typs of programs but how many software design patterns are there? This is a much better analogy I think.
- eksemplar 9y ago
  Wouldn't it be more fair to compare the bridge types to for loops? You need science to come up with it and engineering to apply it in practice.
- bousaid 9y ago
  You can't seriously be putting software engineering above civil or mechanical engineering... They're two completely different fields which both require years and years of training.
bluetwo 9y ago
Because entropy. The natural state of the world is chaos.
- andrepd 9y ago
  That's about meaningless a statement as they come. How do you mean?
  - bluetwo 9y ago
    When you take your nice, theoretical software package and expose it to the real world, you always find things you wouldn't have predicted in the design. The world in general and humans in particular are messy and chaotic. People enter things you wouldn't have expected. People use your software in ways you wouldn't have predicted. Simple communication protocols suddenly become victims of race conditions.
ScottBurson 9y ago
I agree with you about the potential value of formal methods, but I think you completely missed the point of the article. Formal methods can't supply specifications. They can perhaps tell you if your specification is consistent and therefore implementable, but they can't tell you whether the system you've specified will meet your needs. I think those of us who promote formal methods need to remember this. At best only verification -- making sure the implementation matches the specification -- will ever be fully automated. Validation -- making sure that what we specified is actually what we wanted -- will always be a human activity.
- jolux 9y ago
  Yes, you're entirely correct. But you also seem to be the only person in this thread who can pull that distinction out of this discussion, everyone else is ranting about how The Market is the only real spec or whatever.
peteretep 9y ago
> why the author is so suspicious of > formal methods I studied Z-Notation and CSP at what is perhaps the home of formal methods (cs.ox.ac.uk), and I've yet to come across a real-world situation where I've found either in the least bit useful.
auggierose 9y ago
It is right to be suspicious of formal proof. In most areas of software engineering, employing formal proof makes you about 10-1000 times slower. Knowing how to do a formal proof in principle though lets you often reap a lot of the benefit without actually getting slowed down much. This is similar to how mathematicians know how to prove something in principle without running it through Coq or Isabelle. By the way, Curry Howard is just one way of doing formal proof (one I personally don't like). There are many foundational and practical problems that need to be solved before formal proof is ready to go mainstream (but I am convinced that it will one day).

by jolux 9y ago

sillysaurus3 9y ago

Because there are what, six types of bridges? (EDIT: 36 according to wikipedia.) There are six thousand types of programs (as a wild guess), and they all interact with each other in an exponential explosion of complexity. For a formal method to work, it has to be generally applicable across a wide range of situations. There are methods like that in software engineering, and you see them in situations where the program is potentially life-threatening. But most programs would be hindered by this rigor.

rubidium 9y ago
Six types of bridges... Were you serious? There are definitely ways to apply formal engineering methods to software that greatly help its development. Computer programming is not a special snowflake. It's a field that (in many areas) refuses to grow up.
- sillysaurus3 9y ago
  Forcing it to grow up would harm it, though. The engineers would move to companies that don't force those kinds of constraints. It's important to keep in mind what "growing up" translates to: slowing down. This has both economic and competitive implications. Sometimes it might be a win, but the vast majority of the time your ability to move quickly (and yes, occasionally break things) is an advantage.
  - lilott8 9y ago
    Yes and no. It is a natural progression of the industry. Those who cannot do "formal engineering" probably don't belong in engineering roles. Engineering, in general, imho, can be distilled down to this: Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints. If someone as an SE cannot do that, they really have no business being anywhere near any field of engineering.
    - pitay 9y ago
      Depends on the constraints you want to prove that the program will uphold. Some constraints may be impossible to prove, especially in non-real time contexts. For example, a program must run on a platform that doesn't have everything formally defined or have guarantees. If a program relies on that platform and that influences the program in a way that makes the constraint reliant on the platform, then you are out of luck. Another issue is choosing the constraints that the program will operate under. You would hope that the clients would give you the requirements including the constraints the software must operate under. But this isn't often the case. Having an incremental approach which includes clarifying requirements by mapping what the clients need to do to get their work done, which includes recording the specific steps that they perform or need to perform works pretty well when clients don't provide the requirements or constraints upfront. I am relatively ignorant on formal engineering, but I do like that you have provided a fairly clear definition, which was "Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints". It is better than the people saying know more math, without saying how, or what, or why it is useful in any clear way, and saying software is math just doesn't cut it.
      - lilott8 9y ago
        That is a great counter example. I expect there to be a slow migration to platforms like [this formally verified microkernel](https://sel4.systems/ https://sel4.systems/). This will take time and a tremendous amount of effort. But will ultimately address the counter example. In the conclusion of this migration, this puts the SE field into line with the rest of engineering. Choosing the constraints for a project is no different in the context of CS than the context of any other fields -- electrical, mechanical, etc. It is a conversation, as you stated. This helps in many ways: it helps the developer understand exactly what the client wants, helps the client understand exactly what they are going to get, and helps build an implicit timeline replete with discrete and obvious deliverables and (if done correctly) those deliverables are fairly modular. Thanks! I, too, get frustrated that people just say 'math! math! math!' That isn't helpful or meaningful. This is a conclusion I came to after talking to quite a few of my friends and colleagues in different engineering disciplines.
- pvg 9y ago
  It is a special snowflake because the semantics and correctness of nontrivial programs are often in the eye of the beholder (is Microsoft Word or Google Search 'correct'?). This isn't the case for bridges, cars or toasters. It's not just a matter of adding magic engineering dust until programming is engineering.
  - Denzel 9y ago
    No, the correctness is in the eye of a spec. Now, whether companies formally define their specs is a different story. Many startups don't. With that said, if Microsoft Word meets the given spec, then it's correct. One way to prove this correctness is with testing. This is the case for bridges as well. If I hand a spec to an engineering firm requesting a bridge from A to B at any given price. Well then, there's a lot of bridges that satisfy those constraints. Just because many software companies today don't choose to formally specify a spec and prove a programs correctness upon delivery doesn't mean it's a special snowflake. It just means those teams are immature. Sometimes software development doesn't require a mature team. Like most decisions, there's a cost and timing tradeoff.
    - stale2002 9y ago
      The problem with this line of thinking is that the problems that matter are not related to 100% implementing the spec correctly. The problems that matter are in the design of the spec to begin with. The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly. And do you know what the best way is to test whether you got the spec right? You deploy and see if the feature gets traction. The "spec" that matters is the success of the business. And building a product, and releasing it, is the way to formally test if your feature is "correct" according to the spec that is The Market.
      - jolux 9y ago
        >The important part is picking the CORRECT business requirements, NOT in implementing those business requirements correctly. It's both, though. You also can't tell if you've implemented them correctly if you don't have a formal spec.
- deleted 9y ago
  [deleted]
- mpweiher 9y ago
  Actually, it is fundamentally different in that just building the thing / just running the experiment is cheaper than doing the simulations or proofs. Every other discipline does simulations because actually running the experiment is magnitudes more expensive and time consuming. See "Why software development is an engineering discipline" https://www.youtube.com/watch?v=zDEpeWQHtFU
  - TeMPOraL 9y ago
    I agree. The primary thing distinguishing software development from other engineering fields is that the cost of building the product is essentially zero. Because building is what your compiler does. What a programmer does is design, and that is always influenced by the constraints of manufacturing - which, for software, are almost non-existent.
jolux 9y ago
I'll put it this way. In mathematics, the atomic unit of progress is the proof. Proofs are constructed from axioms and other, smaller proofs. The Curry-Howard correspondence is the direct correspondence between computer programs and mathematical proofs. When programming in a well-typed language, everything we do is a degenerate proof of something. I think it's entirely reasonable to try and make it easier to make less degenerate proofs, and encourage the re-centering of proofs as the atomic unit in programming, because they are for programming (as in math) a well-defined, solid formal system that solid systems can be built on in a way that nothing else can be in software, at least thus far. In a world where software flows more freely than water, the correctness and reliability of software systems must be taken with utmost seriousness. This applies to basically any tool that contacts end users, and a lot of ones that don't as well. What do you propose as the theoretical basis for the engineering science of software development?
- sillysaurus3 9y ago
  I think it's self-evident that there is no theoretical basis for software development in the way that would satisfy your criteria. Software dev is generally a scattershot haphazard endeavor that involves trying dozens of angles until one of them works. That's an unsatisfying answer, but if we try to hide from the implications just because we don't like it, we'll end up creating companies that fail to startups without these constraints. It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter.
  - jolux 9y ago
    >I think it's self-evident that there is no theoretical basis for software development in the way that would satisfy your criteria. I don't think this is self-evident whatsoever. One of the problems in software engineering is that we never know when a solution is "right," we only know when it's vaguely not-wrong, and even then almost everything we create is still subtly wrong in a way we forgot to think about. Math is solid because there is certainty in the correctness of certain proofs, and these can be used as building blocks for further results. Philosophically speaking this is the closest we're going to get to "real" engineering practice in software, and we're pretty dang far from it if you know what that looks like. >Software dev is generally a scattershot haphazard endeavor that involves trying dozens of angles until one of them works. But this is a symptom of any pre-scientific field in engineering, it's not specifically endemic to software engineering. The main difference is that in software engineering we're applying math directly, and in other engineering fields we're applying science. In a certain sense, the natural sciences are purely empirical (modulo advanced physics of course, which overlaps with pure math and philosophy these days) while math and consequently computer science are purely rational. So, what are the solid elements in math? Proofs. Proofs are also how you ensure that the field actually moves forward and you're not stuck recreating solid results that already exist. Sound familiar? It happens constantly in software, but imperative and poorly-typed languages inhibit composability and reuse because they lend themselves easily to extremely specific solutions to general problems. >It's also self-evident that in most situations, correctness and reliability aren't a concern. The counterexamples account for maybe 1% of the field. 99% of the time, if your program breaks, you can pay someone to go fix it and no serious harm was done. Even Github outages, which affect almost all of us, hardly matter. This is preposterous. Just because lives are not in danger does not mean that it's not worth doing right by the solution, and frankly I think a lot more lives are waiting to be put in danger by crappy software with bad security than you realize. It's already become almost dogma that all software engineers need to have a deep understanding of security, and I don't understand why correctness can't fall under that rubric as well. If we're going to be having Geohot or even Google or whoever building self-driving cars for possibly billions of people, enormous critical infrastructure projects coming under computer control, etc, the whole industry from education on up is going to have to have a serious attitude adjustment to keep up with the demands of safety, security, and reliability. It might not matter 99% of the time, (I think it's a lot more than that of course) but we need to make sure that we can as a discipline deliver that 1% when it is absolutely critical, and as of right now it doesn't seem like we can.
KirinDave 9y ago
So like, for example, Monads. Monads are applicable across every program ever written and with some rules laid out around them have remarkable properties. Comonads too. Can we use those? By your criteria, I mean.
nautilus12 9y ago
There may be thousands of typs of programs but how many software design patterns are there? This is a much better analogy I think.
eksemplar 9y ago
Wouldn't it be more fair to compare the bridge types to for loops? You need science to come up with it and engineering to apply it in practice.
bousaid 9y ago
You can't seriously be putting software engineering above civil or mechanical engineering... They're two completely different fields which both require years and years of training.

bluetwo 9y ago

Because entropy. The natural state of the world is chaos.

andrepd 9y ago
That's about meaningless a statement as they come. How do you mean?
- bluetwo 9y ago
  When you take your nice, theoretical software package and expose it to the real world, you always find things you wouldn't have predicted in the design. The world in general and humans in particular are messy and chaotic. People enter things you wouldn't have expected. People use your software in ways you wouldn't have predicted. Simple communication protocols suddenly become victims of race conditions.

ScottBurson 9y ago

I agree with you about the potential value of formal methods, but I think you completely missed the point of the article. Formal methods can't supply specifications. They can perhaps tell you if your specification is consistent and therefore implementable, but they can't tell you whether the system you've specified will meet your needs. I think those of us who promote formal methods need to remember this. At best only verification -- making sure the implementation matches the specification -- will ever be fully automated. Validation -- making sure that what we specified is actually what we wanted -- will always be a human activity.

jolux 9y ago
Yes, you're entirely correct. But you also seem to be the only person in this thread who can pull that distinction out of this discussion, everyone else is ranting about how The Market is the only real spec or whatever.

peteretep 9y ago

> why the author is so suspicious of > formal methods I studied Z-Notation and CSP at what is perhaps the home of formal methods (cs.ox.ac.uk), and I've yet to come across a real-world situation where I've found either in the least bit useful.

auggierose 9y ago

It is right to be suspicious of formal proof. In most areas of software engineering, employing formal proof makes you about 10-1000 times slower. Knowing how to do a formal proof in principle though lets you often reap a lot of the benefit without actually getting slowed down much. This is similar to how mathematicians know how to prove something in principle without running it through Coq or Isabelle. By the way, Curry Howard is just one way of doing formal proof (one I personally don't like). There are many foundational and practical problems that need to be solved before formal proof is ready to go mainstream (but I am convinced that it will one day).