Linked by Thom Holwerda on Tue 9th May 2006 21:25 UTC, submitted by luzr
OSNews, Generic OSes Torvalds has indeed chimed in on the micro vs. monolithic kernel debate. Going all 1992, he says: "The whole 'microkernels are simpler' argument is just bull, and it is clearly shown to be bull by the fact that whenever you compare the speed of development of a microkernel and a traditional kernel, the traditional kernel wins. The whole argument that microkernels are somehow 'more secure' or 'more stable' is also total crap. The fact that each individual piece is simple and secure does not make the aggregate either simple or secure. And the argument that you can 'just reload' a failed service and not take the whole system down is equally flawed." My take: While I am not qualified to reply to Linus, there is one thing I want to say: just because it is difficult to program, does not make it the worse design.
Thread beginning with comment 123258
To view parent comment, click here.
To read all comments associated with this story, please click here.
Cloudy
Member since:
2006-02-15

The COSA model is a synchronous model. It is the same model used by logic circuits. Essentially, COSA transforms software into a signaling system comparable to hardware. My claim is simple and is not an extraordinary claim that requires extraordinary proof: if logic circuits can be proven correct, so can COSA programs.

I recommend that the author read David Gries' polemic against "starwars" software development.

Logic circuts can be proven correct (to the extent that they're accepted as never being metastable) because they implement a small enumerable set of state transitions.

You can prove a basic logic circuit correct by inspection of all of its states and transitions in a short period of time.

From this, you can build on the mathematics of formal logic and build up pieces into larger logic circuits and rely on the formalism. This works to a certain level.

But then logic circuits reach a certain level of complexity, and hey presto, they get buggy. (Ever see the errata sheet for a complex processor chip?)

But general software is far more difficult to prove correct. Take a simple mathematical algorithm. It has, in theory, an infinite domain and a potentially infinite range. You can't prove it correct by inspection, and formal techniques don't get you much farther.

Neither of these, however, address Gries' simple but elegant point: You can't prove programs correct, anyway. All you can prove is that they perform according to specification. But that leaves you wondering if the specification is correct....

Reply Parent Score: 3