[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
On 2023-05-27 16:38, Alexander Schreiber via cctalk wrote: 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. I think you have hit the nail on the head there, Alex. not wanting to cause airlines to analyse the cost of extra pilot training and thus compare to the cost of equivalent Airbus product. I have a friend who has a full 737 simulator in his house (no FO seat though) and he put me through a trim runaway. Two toggle switches down on the engine quadrant just disabled the system if the pilots knew what was happening! -- Nigel Johnson, MSc., MIEEE, MCSE VE3ID/G4AJQ/VA3MCU Amateur Radio, the origin of the open-source concept! Skype: TILBURY2591
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
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
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
On 5/25/23 13:38, geneb via cctalk wrote: That wasn't a software problem, that was a criminally cheap management problem - they deleted the comparator for the AoA indexer to save money. Yes, but probably not Boeing's. AoA disagree was an available option that most /airlines/ explicitly elected not to purchase. Part of the AD was requiring that system, plus limiting MCAS authority so that if you hadn't noticed the trim wheel whacking you in the side of the leg you at least couldn't get into a situation where it would take three people to overpower the combined trim and aeroloading forces, and notably, sim time to review trim runaway procedures. It's not reassuring how many crews got trim runaway wrong in the sim. AoA disagreement on the B737 is weird anyway. Each AoA sensor drives one half of the cockpit stall avoidance systems, so the way you typically tell that a sensor has failed is when the stick shaker on one side starts going nuts while the other one doesn't. Honestly, the biggest blame here probably belongs on the doorstep of Southwest. -- Christian Kennedy, Ph.D. ch...@mainecoon.com AF6AP | DB0692 | PG00029419 http://www.mainecoon.comPGP KeyID 108DAB97 PGP fingerprint: 4E99 10B6 7253 B048 6685 6CBC 55E1 20A3 108D AB97 "Mr. McKittrick, after careful consideration…"
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
> On May 25, 2023, at 4:38 PM, geneb via cctalk 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
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
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. g. -- Proud owner of F-15C 80-0007 http://www.f15sim.com - The only one of its kind. http://www.diy-cockpits.org/coll - Go Collimated or Go Home. Some people collect things for a hobby. Geeks collect hobbies. ScarletDME - The red hot Data Management Environment A Multi-Value database for the masses, not the classes. http://scarlet.deltasoft.com - Get it _today_!
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
Just wondering what's marking Guy's posts with ***SPAM***. It's beginning to look like a Monty Python sketch. --Chuck
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
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... --Chuck
[cctalk] Re: ***SPAM*** Re: ***SPAM*** Re: Getting floppy images to/from real floppy disks.
On 5/25/23 10:00, Chuck Guzis via cctalk wrote: On 5/25/23 08:58, Guy Sotomayor via cctalk wrote: ADA and SPARK (a stripped down version of ADA) are used heavily in embedded that has to be "safety certified". SPARK also allows the code to be "proven" (as in you can write formal proofs to ensure that the code does what you say it does). Ask me how I know. ;-) I was aware of Ada's requirements in the defense- and aerospace-related industry. Is that where your experience lies? Is SPARK the "magic bullet" that's been searched for decades to write provably correct code? I'm familiar with it from the higher end automotive perspective (self-driving cars). Even when using C/C++ we have *lots* of standards that we have to adhere to (MISRA, CERT-C, ISO-26262, etc). 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). -- TTFN - Guy
