[nmrm2]

History shows us that "3rd party review process"es turn into paperworks games, with all of the effort going into making sure some boxes are ticked and no effort going into actually thinking about the code. Especially for large code bases operating in complicated domains where the effort required to really understand both the code and its context is at about the same order of magnitude as writing it in the first place.

A 3rd party review can reveal horrid practices, but it's hard-pressed to make any sort of guarantee, no matter how soft.

We know how to do better than "process". Software verification techniques are approaching economical. If a piece of safety-critical software is going to put lives at stake on every road in America, it's reasonable to ask the creator of the software for a set of formal specs that is concise enough it can actually be reviewed by experts, together with a proof that their software meets that formal spec.

[loudmax]

Current history is showing that if the source code isn't revealed, the formal specs will be rigged. Concise formal specs and proofs are a great addition to the source code, but they are not a substitute. Access to source code is even more critical when lives are at stake.

> We know how to do better than "process".

Are you saying that revealing source will lead to more bureaucracy that formal specs will somehow avoid? I don't see how that follows.

[nmrm2]

Open sourcing the code is an orthogonal issue to whether we should consider the use of formal methods a best practice.

> Are you saying that revealing source will lead to more bureaucracy that formal specs will somehow avoid?

I'm arguing that process is insufficient (which, crucially, doesn't imply formal methods are by themselves sufficient, and also doesn't imply process or access to source code isn't necessary).

Merely revealing the source code isn't enough if you need to know how the car behaves and have to recover the meaning of a bunch of complicated equations in order to make any sense of the code. Really reading and trusting the code would require more effort than re-writing it.

> Current history is showing that if the source code isn't revealed, the formal specs will be rigged

Hm. That's very surprising to me. Can you give an example of a company providing a rigged formal spec?

Also, rigging formal specs is why the formal specs should be reivewed by a third party expert.

And if/when fraud does happen (e.g., by giving a bunk formal spec or cheating on the proof), formal methods still have two advantages over process:

* The debate over whether enough work went into QC becomes trivial, and skimping on QC becomes willful deceit (something that's incredibly hard to demonstrate in the status quo).

* Unlike process, there are technical solutions to the problem of rigging proofs. And, the specs themselves are much easier to review than the code. So the review process is pretty likely to catch cheating.

[patsplat]

Agreed why add process when financial and criminal liability would suffice. Add sufficient liability and players will improve their internal processes appropriately.

[cptskippy]

I think the Bookout v. Toyota case is a pretty good example of how culpability alone is an insufficient motivator and how an add process (e.g. external audit) could have prevented a tragedy.

Michael Barr's review of Toyota's ECU code (http://www.safetyresearch.net/Library/BarrSlides_FINAL_SCRUB...) showed numerous compliance issues with established industry best practices (80,000 violations of MISRA-C) and failure to even follow Toyota's much laxer internal coding standards (32% rule violation). Toyota shipped uncertified versions of their code and the design and behavior of that code prevented defect detection.

[patsplat]

External audits meant nothing with Enron. Criminal liability is the key.

[JoBrad]

I agree. The US legal system has historically been way more lenient on financial companies than automobile companies. In the case of Enron, they had a lot of financial incentive for their actions, with only the prospect of a few fines as the expected downside. I don't see that being the case for GM, Toyota, etc.

[tomtang0514]

Because they're slightly different cases considering how they begin. The GM and Toyota cases are that they screwed up. They failed to design a safe system. Meanwhile this VW case and those financial cases are that they designed the system intentionally to screw up other people. It's like accidental homicide vs murder.

[imglorp]

You need more than this. GM just off scott-free after killing and wounding hundreds with the ignition switch malfeasance. The company plead down to do some PR and pay a teensy fine. Meanwhile, the murderers among them were not charged.

[w_t_payne]

Depends on how it is managed.

[nmrm2]

Definitely. Formal methods don't replace process carte blanc, but rather make the tasks from which the review process is composed tractable.