5 ms·

Which is why I don't buy the "software has only been around for 70 years so give it time" argument. Software has nothing to be grounded in like other engineers

Which is why I don't buy the "software has only been around for 70 years so give it time" argument. Software has nothing to be grounded in like other engineers do with physics. It's most likely always going to be endless cargo culting.

choeger 5y ago
That's simply not true. Software is grounded in mathematics. Most people just try to ignore that fact for convenience. There are, for instance, famous books written about which errors can be proven to be absent in your program and how (vulgo typechecking). There is a huge amount of research about data structures and their internal logic (and at least one, very weird observation about the meaning of the derivatives of data structures). And I don't need to mention complexity theory, do I? Just because a huge part of the practitioners ignores the scientific base of our discipline doesn't mean it doesn't exist.
- TuringTest 5y ago
  As an oficially qualified computer scientist, I can say that software is grounded in mathematics, but this does not imply what you're thinking. *All* formalisms, including mathematics, are in the end nothing but an incredibly precise language to talk about ideas in your head. Programming languages are created for communication, so this is specially true for them. The fact that code has an extremely precise semantics comes from it being a formal system. But its close relation with maths and physics, besides that they are all formal systems, is mainly because mathematicians and physicists were the first to create it; it's mostly a matter of tradition. There are ways to create, use and study software that are closer to language studies than they are to math, and those are legitimate comp-sci too. Non-formal aspects of building software, like which style guide to establish in your organization, are part of the discipline even if you don't use math to study them. Formal proof is a convenient way to check that your detailed, precise assertions are consistent with your initial axioms. This doesn't prove at all that there are no errors in your code, only that there are no contradictions in what you are saying. Your specification could still be wrong, and then you could still be saying the wrong thing in terms of what you intend to say or achieve; and the formalism won't help. It is not surprising that managers gets to decide how software is built in their department. Software is an explanation of concepts with a particular style, and those who set the tone implant their quirks in it. You're building what the manager tells you to build, and end using the same language.
  - Drew_ 5y ago
    > Formal proof is a convenient way to check that your detailed, precise assertions are consistent with your initial axioms. This doesn't prove at all hat there are no errors in your code, only that there are no contradictions in what you are saying. Your specification could still be wrong, and then you could still be saying the wrong thing in terms of what you intend to say or achieve; and the formalism won't help. Software assurance is still a somewhat nebulous process and I'm partly involved in some research around it and proving that a program is logically sound is indeed only a small piece of the pie and hardly gets you anywhere valuable. FizzBuzz is provably logical, but that doesn't mean you can load FizzBuzz onto a space shuttle and expect it to fly correctly.
    - TuringTest 5y ago
      Great example! How does research in software assurance treats the human side of behaviors and desires, which can't be formalized? Are there protocols that can increase reliability for an established purpose?
      - Drew_ 5y ago
        Many times there are authorities that have formalized protocols for systems involving people. For example, the FAA has prescribed thresholds where pilots should be alerted of possible failures when navigation system measurements have exceeded those thresholds. Other times thresholds like those can be found just through user testing and feedback. The goal there is to ensure safety without losing the confidence of the user or overwhelming them with information. There are a number of general Software Assurance protocols. I'm not super familiar with them, but DO-178C is one I hear about often which is a process specifically for assuring/certifying airborne systems.
dtech 5y ago
It's more like mathematics. While it's true that everyone can invent their own maths, this is only really done in advanced academia for research. Almost everything in practical use is standarized. No-one is arguing about whether you need integration or what the right notation for differential equations is. This took time to achieve. You wouldn't be able to read Newton's papers easily, even though a large amount of high school mathematics is based on things he invented/discovered.

choeger 5y ago

That's simply not true. Software is grounded in mathematics. Most people just try to ignore that fact for convenience. There are, for instance, famous books written about which errors can be proven to be absent in your program and how (vulgo typechecking). There is a huge amount of research about data structures and their internal logic (and at least one, very weird observation about the meaning of the derivatives of data structures). And I don't need to mention complexity theory, do I? Just because a huge part of the practitioners ignores the scientific base of our discipline doesn't mean it doesn't exist.

TuringTest 5y ago
As an oficially qualified computer scientist, I can say that software is grounded in mathematics, but this does not imply what you're thinking. *All* formalisms, including mathematics, are in the end nothing but an incredibly precise language to talk about ideas in your head. Programming languages are created for communication, so this is specially true for them. The fact that code has an extremely precise semantics comes from it being a formal system. But its close relation with maths and physics, besides that they are all formal systems, is mainly because mathematicians and physicists were the first to create it; it's mostly a matter of tradition. There are ways to create, use and study software that are closer to language studies than they are to math, and those are legitimate comp-sci too. Non-formal aspects of building software, like which style guide to establish in your organization, are part of the discipline even if you don't use math to study them. Formal proof is a convenient way to check that your detailed, precise assertions are consistent with your initial axioms. This doesn't prove at all that there are no errors in your code, only that there are no contradictions in what you are saying. Your specification could still be wrong, and then you could still be saying the wrong thing in terms of what you intend to say or achieve; and the formalism won't help. It is not surprising that managers gets to decide how software is built in their department. Software is an explanation of concepts with a particular style, and those who set the tone implant their quirks in it. You're building what the manager tells you to build, and end using the same language.
- Drew_ 5y ago
  > Formal proof is a convenient way to check that your detailed, precise assertions are consistent with your initial axioms. This doesn't prove at all hat there are no errors in your code, only that there are no contradictions in what you are saying. Your specification could still be wrong, and then you could still be saying the wrong thing in terms of what you intend to say or achieve; and the formalism won't help. Software assurance is still a somewhat nebulous process and I'm partly involved in some research around it and proving that a program is logically sound is indeed only a small piece of the pie and hardly gets you anywhere valuable. FizzBuzz is provably logical, but that doesn't mean you can load FizzBuzz onto a space shuttle and expect it to fly correctly.
  - TuringTest 5y ago
    Great example! How does research in software assurance treats the human side of behaviors and desires, which can't be formalized? Are there protocols that can increase reliability for an established purpose?
    - Drew_ 5y ago
      Many times there are authorities that have formalized protocols for systems involving people. For example, the FAA has prescribed thresholds where pilots should be alerted of possible failures when navigation system measurements have exceeded those thresholds. Other times thresholds like those can be found just through user testing and feedback. The goal there is to ensure safety without losing the confidence of the user or overwhelming them with information. There are a number of general Software Assurance protocols. I'm not super familiar with them, but DO-178C is one I hear about often which is a process specifically for assuring/certifying airborne systems.

dtech 5y ago

It's more like mathematics. While it's true that everyone can invent their own maths, this is only really done in advanced academia for research. Almost everything in practical use is standarized. No-one is arguing about whether you need integration or what the right notation for differential equations is. This took time to achieve. You wouldn't be able to read Newton's papers easily, even though a large amount of high school mathematics is based on things he invented/discovered.