On May 25, 2023, at 4:38 PM, geneb via cctalk
<cctalk(a)classiccmp.org> wrote:
On Thu, 25 May 2023, Chuck Guzis via cctalk wrote:
On 5/25/23 10:06, Guy Sotomayor via cctalk
wrote:
The way SPARK works is that you have code and
then can also provide
proofs for the code. Proofs are you might expect are *hard* to write
and in many cases are *huge* relative to the actual code (at least if
you want a platinum level proof).
...and we still get gems like the Boeing 737MAX...
That wasn't a software problem, that was a criminally cheap management
problem - they deleted the comparator for the AoA indexer to save money.
So? We know managers often don't know engineering or reliability, that's why we
have engineers. It's not just the job of the engineer to follow orders; it's also
his job to make the right thing happen, and to complain if it isn't.
Engineers keeping quiet has been a key contributor in many spectacular failures, from the
737 MAX to the two Space Shuttle failures.
paul