| 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. |