3 ms·
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
by 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 agoGreat 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 agoMany 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.