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