I refer you to Joel Spolsky about formal proofs of programs:

[…]

So in the first day of that class, Dr. Zuck filled up two entire whiteboards and quite a lot of the wall next to the whiteboards proving that if you have a light switch, and the light was off, and you flip the switch, the light will then be on.

The proof was insanely complicated, and very error-prone. It was harder to prove that the proof was correct than to convince yourself of the fact that switching a light switch turns on the light. Indeed the multiple whiteboards of proof included many skipped steps, skipped because they were too tedious to go into formally. Many steps were reached using the long-cherished method of Proof by Induction, others by Proof by Reductio ad Absurdum, and still others using Proof by Graduate Student.

For our homework, we had to prove the converse: if the light was off, and it’s on now, prove that you flipped it.

I tried, I really did.

I spent hours in the library trying.

After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, this mechanism would never be able to prove things that are interesting.

https://www.joelonsoftware.com/2005/01/02/advice-for-compute...

I have a MSc in formal methods, and this is really misleading. Surely you cannot make some proofs easily. However, how did Airbus verify that some errors simply do not exist in their fly-by-wire software (which is ~100 KLOC implemented in a subset of C)? (I'm sure Boeing also employs these techniques internally).

Using abstract interpretation. There are tons of formal methods, ranging from type systems to formal proofs. Lots of compromises can be made to make them practical and useful for a particular domain. Look into [1,2] for some quick introductory examples. Going straight into formal proofs is in general a really bad idea.

I have worked on railway control systems, with really nasty potential race conditions and managed to prove the absence of large classes of errors. Then derived implementations formally. It's really not that hard. There's even a subfield of CS looking into verifying formal properties of biological systems [3], which are really complex.

[1] http://adam.chlipala.net/frap/

[2] http://www.concrete-semantics.org/

[3] http://lucacardelli.name/Papers/Abstract%20Machines%20of%20S...

I wonder if anyone can follow Feynman’s style of proof?

By the end of that summer of 1983, Richard had completed his analysis of the behavior of the router, and much to our surprise and amusement, he presented his answer in the form of a set of partial differential equations. To a physicist this may seem natural, but to a computer designer, treating a set of boolean circuits as a continuous, differentiable system is a bit strange. Feynman's router equations were in terms of variables representing continuous quantities such as “the average number of 1 bits in a message address.” I was much more accustomed to seeing analysis in terms of inductive proof and case analysis than taking the derivative of “the number of 1’s” with respect to time.

http://longnow.org/essays/richard-feynman-connection-machine...

As explained in this talk by Robert Martin, proving programs correct was the big goal which Edsger W. Dijkstra tried to reach by eliminating GOTO in favor of structured programming (which is essentially having if-else statements, loops and iteration as part of a language as replacement for all practical uses of GOTO).

https://www.youtube.com/watch?v=SVRiktFlWxI#t=2h9m38s

Software could be proven correct, but we abandoned that, just gave up on it, it’s too hard. But we can test it. We can use science, and we can write tests that demonstrate that the software is not failing. We treat software like a science, not like mathematics.

— Robert Martin

I think Robert Martin doesn't fully grasp the field of formal methods and program semantics, which has evolved a lot since the early 1980s. Paraphrasing Alan Perlis, beware of the Turing tar pit, where everything is possible but nothing of interest is easy.

So one trick is to work on DSLs with restricted semantics that are good enough for your domain. That makes proofs plus other formal techniques, and hence security guarantees, much much easier.

But if you insist on Turing complete languages, as I explained above, you can e.g. build abstract interpreters or data flow analyses that are able to prove really sophisticated things. I have implemented a C abstract interpreter for an industrial client that among many other things detected whether you were making potential out of bounds accesses to arrays, or potentially using uninitialized pointers. Of course it erred on the safe side. But it was really precise (few false positives). Not a walk in the park as it relies on Galois connections. See the seminal Cousot & Cousot 1977 paper [1].

[1] https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml

I'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one needs to write to get anything done. For reference, the certified compiler CompCert's code base is something like 10% code and 90% proofs.

Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements.

You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!).

Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well!

I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.

This. MCAS was the wrong thing to build. The wrong thing, correctly built, is still wrong, no matter how perfect the formal verification.

So true. The problem is in the system at a higher level. It is not really a software defect that killed all those folks.

It would ensure people thought about it a lot longer and harder than without those proofs, so the code had a whole lot more critical thinking done over it. Seems worth it in some areas like airplanes.

The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do.

MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” and ended up with the exact same result.

A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.

Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.

I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.

Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered.

I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.

Two sensors is enough if you can shut off the system when they disagree. MCAS didn’t doom the plane if it shut off, so that was enough. The problem was that they didn’t do this, and instead used only one sensor at a time. Basic sense and standard practice tells you not to do that. I don’t know if more formality would have helped them not do something so boneheaded.

However, this looks like an unusual case. Based on the fact that they had such a dumb design for this system, that shouldn’t have passed muster in any aviation context no matter your software methodology, it’s probably not representative enough to draw a larger lesson about engineering. The larger lesson seems to be business and regulatory.

Regarding Japanese cars, Toyota went through a big thing with unintended acceleration that got quite a few people killed. Software was suspected, but the cause was ultimately determined to (mostly?) be a combination of drivers mixing up the accelerator and the brake (happens more often than you might think) and unsecured floor mats pushing the accelerator down. I bought a Toyota not too long after this and the dealer made a special point to show me how the floor mat attached to the floor and that I must be sure it was solidly connected.

Their software was audited and apparently it was really badly made. It was described as “spaghetti-like” and had global variable abuse, ignored errors, failed to restart unresponsive tasks, and had potential memory corruption problems. It’s quite possible that this really was the cause, and a jury even found this to be the cause in a civil trial over one of the crashes, but it was never definitely linked.

It also makes absolutely no sense in any software that works entirely with and relies on external, mechanical hardware sensors. There is a reason people use this to certify their operating system or algorithm works: you can forever stay in a bubble that your processor is just a big math machine, no external inputs, no external outputs. We have "certified secure" operating systems that nonetheless are trivially attacked through something like rowhammer.

How do you solve it? Assume your AoA sensor is always correct? Congratulations, MCAS is a provably correct solution! Make the sensor behavior more complex? Sorry, the problem is now intractably complex (and still doesn't model the actual hardware).

If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verify the software itself, so how does that help?

In a type checked language. Your software is guaranteed to have no type errors. How hard was that?

That's a great example! It illustrates the point in a better way than I tried to.

A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself.

If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.

No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.

Well, to support the top parent's comment, here's what John Carmack had to say about SAAB's fighter jet:

> The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling it what to do, but this worked out well for testing: all data was allocated statically, and monitoring those variables gave a clear picture of most everything the software was doing. The software did only the bare essentials, and of course, they were serious about thorough ground testing.

> No bug has ever been found in the “released for flight” versions of that code.

so not quite that tests are useless because blackbox, but more that yes, it is possible to write software that facilitates showing a code will do what it says it will do.

In another note, I do feel sorry for the engineers but at the same time Airbus also has similar MCAS system, but the only thing that saves them is an extra Angle-of-Attack sensor whereas I believe the boeing relied on just one or two. Airbus had 3 AOA sensors and if 2 agreed, that was the data fed into the MCAS.

It still boggles my mind that they would place a bigger engine when the original plane was not built for it at all, this was 100% profit orientated move to prevent Airbus from taking Boeing's majority marketshare, it's highly ironic that the opposite results.

Even more infuriating is that Boeing passed it off as the exact same plane, not much extra training is necessary, along with FAA giving their blessing, now caught up in the mess.

Canada for instance is now looking to the EU for an independent auditing, as any credibility FAA has built up over the past years has taken a significant hit.

Interesting quote. Seems it was actually a quote of Henry Spencer by Carmack. http://number-none.com/blow/john_carmack_on_inlined_code.htm...

Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability

huh? interesting, do you have more info, I love reading stuff like this. I don't know much about the Gripen but it is my all time favorite after the F-16.

Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew:

https://www.youtube.com/watch?v=49L9BlYQSjw

The first crash: https://www.youtube.com/watch?v=k6yVU_yYtEc

Second crash (over middle of Stockholm) https://youtu.be/mkgShfxTzmo?t=133

From Wikipedia: During the test programme, concern surfaced about the aircraft's avionics, specifically the fly-by-wire flight control system (FCS), and the relaxed stability design. On 2 February 1989, this issue led to the crash of the prototype during an attempted landing at Linköping; the test pilot Lars Rådeström walked away with a broken elbow. The cause of the crash was identified as pilot-induced oscillation, caused by problems with the FCS's pitch-control routine.[22][33][34]

In response to the crash Saab and US firm Calspan introduced software modifications to the aircraft. A modified Lockheed NT-33A was used to test these improvements, which allowed flight testing to resume 15 months after the accident. On 8 August 1993, production aircraft 39102 was destroyed in an accident during an aerial display in Stockholm. Test pilot Rådeström lost control of the aircraft during a roll at low altitude when the aircraft stalled, forcing him to eject. Saab later found the problem was high amplification of the pilot's quick and significant stick command inputs. The ensuing investigation and flaw correction delayed test flying by several months, resuming in December 1993.[22]

can't believe the first one didn't result in a ball of fire...

the second was even more shocking, all of a sudden it looked like he was trying a Cobra maneuver until he ejected! that's insane.

Isn't Airbus's a stick pusher, though? i.e. it puts force on the stick that is hard to overpower but can be overpowered, so the pilot is still the control authority?

That's extremely different to a system that silently severely mistrims you, then tells you to disable your ability to trim electrically before you can fix the mistrim, as if that even makes sense, all while overpowering the yoke with aerodynamic load.

For the record, Airbus's three sensors haven't prevented crashes completely. Here's one where two sensors were damaged, causing the correct sensor to be treated as erroneous and lose the quorum vote:

https://en.wikipedia.org/wiki/XL_Airways_Germany_Flight_888T

What saves Airbus is the extra MCAS system, and a stronger regulatory environment, and most importantly a jet that has the engines mounted in the proper place so it doesn't have a tendency to stall.

I don't know about modern systems but PLC's (industrial controllers) worked exactly this way when I worked with them in the 90s. You can introduce subtle bugs with these either.

Interesting about the SAAB fighter. Essentially the opposite of spaghetti code? One really long spaghetti straw that is uncooked?

I like really long function bodys so I get turned on by the idea.

Proving that software matches the spec is one thing, proving that the spec is free of bugs is quite another.

Indeed. It is normal that implementation will find a bug in the spec. Anecdotally, have never found a flawless RFC. Every real-world implementation of an RFC I've ever done has found some discrepancy when it came to compatibility testing.

Yes. But for critical software systems, what excuse does one have not to prove that the software does not match the spec. There is no excuse not to test the spec, but what excuse is there not to prove the software?

Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.

No, we can literally prove it correct based off of a specification.

https://en.wikipedia.org/wiki/Correctness_(computer_science)

In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.

If the spec is complex you are probably proving the bugs in the spec are indeed correctly implemented...

Edit: that said, spending the formal spec time will probably reduce the number of bugs far below than what we find normal now. But money...

Yeah and then the specification at that level of specificity IS the code. How do you prove the specification is bug free?

Define what is a bug in a spec? I defined the program to do one thing and one thing only. What does does it mean when I have a bug in my definition? There's a definition for the definition? Makes no sense.

You can argue that no code ever has bugs by that logic, after all you defined the program to do one thing, and it did it, it was merely human expectation that was in error.

That's what I'm arguing. Code can be proven correct against a formal spec.

However, because we don't do proofs in software, there are bugs.

Code is itself a specification.

It can be, but generally it is not.

It means that the one thing you defined it to do was not the right thing.

> Bugs can arise where programs intersect in the real world.

Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness.

But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)

You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.

Proving something is correct is only part of the problem. A random bit flip (no matter amount of error correction and physical hardening) and your proven-correct software goes amok. And this is just one of the many issue you can encounter dealing with the physical world.

Ironically, the solution to this in spacecraft, where radiation is a given, is 2 of 3 with polling.

The system which should have been using for attitude detection in the 737 MAX, and wasn't.

Dosen't eliminate a single point of failure, after all a bitflip in the voting mechanism can also result in error.

Yeah, you're right. Can't completely get rid of tests but the irony still exists.

Mathematicians often don't rely on the exact correctness of a proof's description, instead relying on a rough sketch of strategy.

Isn't digital logic testing a thing for hardware?

Complex hardware often contains bugs many of which map to software bugs. Hardware though tends to be highly constrained in how it's operated.

Man: Doc it hurts when I bend my knee this way.

Doc: Well don't do that.

EE: The hardware state machine runs into the weeds when given these inputs.

Tech Rep: Yeah don't do that.