On Thu, May 25, 2023 at 12:30:52PM -0700, 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 was Working As Implemented. Turns out, if you change the way
the aircraft behaves under some conditions and you can't be bothered
to tell the pilots about it, bad things are eventually going to happen.
Bonus points for making safety related features extra-cost items
(so your cheaper airlines won't buy them, with predictable results).
Extra bonus points for having achieved regulatory capture and so
being allowed to handwave "It will be fine, trust us" the certifications.
One long term result is that European agencies learned to no longer
trust the FAA.
The root cause was that Boeing was trying to do things on the cheap,
going "This is still your fathers old 737, just a little spruced up"
when it was effectively a different plane - but admitting that would
have triggered lots of expensive things (certifications, pilot training
for a new aircraft, ...).
There are businesses where you can get away with being cheap and
there are types of business where a little extra profit will be
paid for with _someones_ blood.
Kind regards,
Alex.
--
"Opportunity is missed by most people because it is dressed in overalls and
looks like work." -- Thomas A. Edison
