4 ms·

> The root problem is the assumption that specifications can be validated for correctness, like a blueprint for a bridge can. We can validate specifications fo

> The root problem is the assumption that specifications can be validated for correctness, like a blueprint for a bridge can. We can validate specifications for correctness with automated theorem proving! The least we can do is model-checking. At least for the hard algorithms and core system interactions. We've had this ability for decades. The problem with software development is that we get all hand-wavy about "architecture," and "design." I try not to physically groan when someone starts sketching out a box diagram. They're fancy pictures, sure, and useful at a conceptual level... but the reality is that the software will look nothing like that diagram. And there's no way to check that the diagram is even correct! Useless! It doesn't have to be painfully slow, burdensome, and expensive to employ these tools either. Contrary to popular belief it doesn't take a team of highly trained PhD physicists to build a formal mathematics for modelling computations these days. There are plenty of open-source tools for using languages like TLA+ that work great besides! Ask Amazon -- they published a paper about it. Watch Leslie Lamport - Who Builds a Skyscraper without Drawing Blueprints?: https://www.youtube.com/watch?v=iCRqE59VXT0 https://www.youtube.com/watch?v=iCRqE59VXT0

2muchcoffeeman 10y ago
I draw pictures because I think in pictures. I just took a short look at TLA+ and read a tutorial. Don't think I could use it without drawing a picture.
- agentultra 10y ago
  Drawing a picture is a perfectly valid and legitimate start. However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them. A sketch is still useful the the absence of nothing else. But we don't build bridges and skyscrapers that way so why is it good enough for our data-centres and applications? I don't think lives have to be on the line in order for software to be considered harmful if not built correctly. There are plenty of problems where having a thoroughly checked design will save you plenty of headaches and afford you many more opportunities.
  - mikekchar 10y ago
    > However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them. It's necessary to have a formal language to describe this design. Such a formal language needs to have one and only one interpretation. We should be able to take a document written with that formal language and verify that it meets our assumptions. We should also be able to verify that the final implementation is isomorphic to the design. Luckily such tools are ubiquitous. You can use whatever programming language you like to specify your design. In the case where the programming language is defined poorly, then you must also decide what build system and run time environments you will support ahead of time. You can document your assumptions using the same programming language. This is made easier if you use a "test framework", but if needed you can also roll your own. You can validate your design by running the tests against your design. Normally it is best to break up your design into "units" that make it more clear how to validate your assumptions. You can then add some extra validation that the composition of "units" transitively validates your assumptions. You can verify that your final produce adheres to that design because there will be a 1:1 mapping from the design to the final product (i.e. the final product will be implemented using the same code as your design). There are wonderful tools that will tell you the "coverage" of code used in the final product that has been validated against the assumptions. Finally, you can even specify your requirements using the same formal language and verify that the design meets the requirements. Normally you do this by validating that the "integration" of "units" meets your assumptions. This should not be done without individually validating the assumptions on the "units", though, because the "integration" can lead to exponentially growing alternatives. Normally it is infeasible to validate each alternative. Yes, this reply is tongue in cheek, but I am not ignorant of formal specification methods. They have their place. That place is currently not in a professional software development shop. We have better methods at the moment. Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.
    - agentultra 10y ago
      > Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet. I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0]. Perhaps it is because there are myths that are still floating around regarding formal methods that still make developers cringe when they hear mention of them [1]. None the less I couldn't find reference to it in the book... did I miss it? And besides... unit tests, I'm sure you are aware, aren't good enough alone. They can only increase your confidence in an implementation but they prove nothing. If we want to start calling ourselves engineers I think we better start looking to how the other engineering disciplines operate. I don't think it will be long before an insurance company comes along and finds actuaries capable of monitoring risk in software development projects and liability becomes a necessary concern. [0] http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo... [1] http://www.fm4industry.org/index.php/G-HM-2 http://www.fm4industry.org/index.php/G-HM-2
- nickpsecurity 10y ago
  Statecharts. Processing. UML model-driven development.
  - eternalban 10y ago
    I was under the impression UML gave up the ghost(?)
    - nickpsecurity 10y ago
      There's literally millions in commercial and academic activity around it. Maybe tens of millions. It's not dead yet despite me wishing it never had life to begin with haha.
  - nickbauman 10y ago
    None of which can be validated for correctness.
    - nickpsecurity 10y ago
      Really? First results on Google: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.6717 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.... http://researcher.watson.ibm.com/researcher/files/il-RONENL/FVforUML.pdf http://researcher.watson.ibm.com/researcher/files/il-RONENL/... I've seen plenty more work on UML as academics & commercial vendors are still all over it. I couldn't find an example for "Processing" because they picked the stupidest name possible: a word so overused I'm getting results from the food industry, compilers, IRS, and computers all at once.
      - nickbauman 10y ago
        When you can build a system from UML, let's talk about that "formal provability" again.
        nickpsecurity 10y ago
Retra 10y ago
Formal validation are perfect for when you know exactly what problems you're solving. Unless a business is offering a very specific solution like that, then it won't help them. If you're writing security software or low-level system controls or something. But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient. >There are plenty of open-source tools for using languages like TLA+ that work great besides! Does your team know TLA+? Is it an efficient use of their time to learn it? Are a bunch of TLA+ beginners going to crank out properly written software?
- agentultra 10y ago
  > Formal validation are perfect for when you know exactly what problems you're solving. Or you're at the point where formal validation is a requirement. There's nothing stopping one from using any of these tools as design tools. I'm working on a problem to check whether items delivered by a single producer on a FIFO queue with N workers can guarantee all work items will eventually be attended to. I could just write the code for that but I'll never prove the system works that way. The best one can do is gain confidence that for the prescribed scenarios it will work. You can get good coverage and use all of the tools we know to release something others may decide to use... but then you'll be fixing your errors after the fact when they are discovered and reported by your users. Or in the case of a system as large as AWS you may find that obscurity is no longer a comforting buffer... 1 in 100000 becomes a frequent occurrence. update: There's nothing preventing you from only using formal methods on the critical parts of your system where a high degree of reliability is useful. One does not need to formally verify everything to gain the benefits. > But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient. I think it depends on the difficulty of the problems you address with your software. If you're just sorting some lists or making system calls you might not want to bother. However if you want to guarantee consensus in the face of delays and partitions you'll need more than code to make any strong claims of efficacy. And if the public interest relies on your system I think it's necessary to serve them in the best capacity using the state of the art tools. > Does your team know TLA+? Is it an efficient use of their time to learn it? No. They could pick it up in a couple of weeks if necessary. It is an efficient use of their time: fewer bugs at scale means less downtime and less time spent chasing errors that slipped through. > Are a bunch of TLA+ beginners going to crank out properly written software? Are a bunch of beginner programmers going to crank out properly written software? There are different levels of experience and skill on any team. With training and diligence even beginners can learn to adopt the skill and ability to recognize when and where to use high level specifications and how to abstract systems into mathematical models they can test and prove. Until then I suppose we have to live in a world where security breaches are common and the recall rates on cars will continue to increase as unreliable software continues to cause failures, lives, etc.

2muchcoffeeman 10y ago

I draw pictures because I think in pictures. I just took a short look at TLA+ and read a tutorial. Don't think I could use it without drawing a picture.

agentultra 10y ago
Drawing a picture is a perfectly valid and legitimate start. However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them. A sketch is still useful the the absence of nothing else. But we don't build bridges and skyscrapers that way so why is it good enough for our data-centres and applications? I don't think lives have to be on the line in order for software to be considered harmful if not built correctly. There are plenty of problems where having a thoroughly checked design will save you plenty of headaches and afford you many more opportunities.
- mikekchar 10y ago
  > However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them. It's necessary to have a formal language to describe this design. Such a formal language needs to have one and only one interpretation. We should be able to take a document written with that formal language and verify that it meets our assumptions. We should also be able to verify that the final implementation is isomorphic to the design. Luckily such tools are ubiquitous. You can use whatever programming language you like to specify your design. In the case where the programming language is defined poorly, then you must also decide what build system and run time environments you will support ahead of time. You can document your assumptions using the same programming language. This is made easier if you use a "test framework", but if needed you can also roll your own. You can validate your design by running the tests against your design. Normally it is best to break up your design into "units" that make it more clear how to validate your assumptions. You can then add some extra validation that the composition of "units" transitively validates your assumptions. You can verify that your final produce adheres to that design because there will be a 1:1 mapping from the design to the final product (i.e. the final product will be implemented using the same code as your design). There are wonderful tools that will tell you the "coverage" of code used in the final product that has been validated against the assumptions. Finally, you can even specify your requirements using the same formal language and verify that the design meets the requirements. Normally you do this by validating that the "integration" of "units" meets your assumptions. This should not be done without individually validating the assumptions on the "units", though, because the "integration" can lead to exponentially growing alternatives. Normally it is infeasible to validate each alternative. Yes, this reply is tongue in cheek, but I am not ignorant of formal specification methods. They have their place. That place is currently not in a professional software development shop. We have better methods at the moment. Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.
  - agentultra 10y ago
    > Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet. I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0]. Perhaps it is because there are myths that are still floating around regarding formal methods that still make developers cringe when they hear mention of them [1]. None the less I couldn't find reference to it in the book... did I miss it? And besides... unit tests, I'm sure you are aware, aren't good enough alone. They can only increase your confidence in an implementation but they prove nothing. If we want to start calling ourselves engineers I think we better start looking to how the other engineering disciplines operate. I don't think it will be long before an insurance company comes along and finds actuaries capable of monitoring risk in software development projects and liability becomes a necessary concern. [0] http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo... [1] http://www.fm4industry.org/index.php/G-HM-2 http://www.fm4industry.org/index.php/G-HM-2
nickpsecurity 10y ago
Statecharts. Processing. UML model-driven development.
- eternalban 10y ago
  I was under the impression UML gave up the ghost(?)
  - nickpsecurity 10y ago
    There's literally millions in commercial and academic activity around it. Maybe tens of millions. It's not dead yet despite me wishing it never had life to begin with haha.
- nickbauman 10y ago
  None of which can be validated for correctness.
  - nickpsecurity 10y ago
    Really? First results on Google: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.6717 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.... http://researcher.watson.ibm.com/researcher/files/il-RONENL/FVforUML.pdf http://researcher.watson.ibm.com/researcher/files/il-RONENL/... I've seen plenty more work on UML as academics & commercial vendors are still all over it. I couldn't find an example for "Processing" because they picked the stupidest name possible: a word so overused I'm getting results from the food industry, compilers, IRS, and computers all at once.
    - nickbauman 10y ago
      When you can build a system from UML, let's talk about that "formal provability" again.
      - nickpsecurity 10y ago

Retra 10y ago

Formal validation are perfect for when you know exactly what problems you're solving. Unless a business is offering a very specific solution like that, then it won't help them. If you're writing security software or low-level system controls or something. But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient. >There are plenty of open-source tools for using languages like TLA+ that work great besides! Does your team know TLA+? Is it an efficient use of their time to learn it? Are a bunch of TLA+ beginners going to crank out properly written software?

agentultra 10y ago
> Formal validation are perfect for when you know exactly what problems you're solving. Or you're at the point where formal validation is a requirement. There's nothing stopping one from using any of these tools as design tools. I'm working on a problem to check whether items delivered by a single producer on a FIFO queue with N workers can guarantee all work items will eventually be attended to. I could just write the code for that but I'll never prove the system works that way. The best one can do is gain confidence that for the prescribed scenarios it will work. You can get good coverage and use all of the tools we know to release something others may decide to use... but then you'll be fixing your errors after the fact when they are discovered and reported by your users. Or in the case of a system as large as AWS you may find that obscurity is no longer a comforting buffer... 1 in 100000 becomes a frequent occurrence. update: There's nothing preventing you from only using formal methods on the critical parts of your system where a high degree of reliability is useful. One does not need to formally verify everything to gain the benefits. > But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient. I think it depends on the difficulty of the problems you address with your software. If you're just sorting some lists or making system calls you might not want to bother. However if you want to guarantee consensus in the face of delays and partitions you'll need more than code to make any strong claims of efficacy. And if the public interest relies on your system I think it's necessary to serve them in the best capacity using the state of the art tools. > Does your team know TLA+? Is it an efficient use of their time to learn it? No. They could pick it up in a couple of weeks if necessary. It is an efficient use of their time: fewer bugs at scale means less downtime and less time spent chasing errors that slipped through. > Are a bunch of TLA+ beginners going to crank out properly written software? Are a bunch of beginner programmers going to crank out properly written software? There are different levels of experience and skill on any team. With training and diligence even beginners can learn to adopt the skill and ability to recognize when and where to use high level specifications and how to abstract systems into mathematical models they can test and prove. Until then I suppose we have to live in a world where security breaches are common and the recall rates on cars will continue to increase as unreliable software continues to cause failures, lives, etc.