13 ms·
...said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel... In this case, exactly what does "mathemati
by edw519 17y ago
...said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel...
In this case, exactly what does "mathematical rigour" mean? I imagine there are several responses to this question, but even a conceptual overview of how math can prove bug-freeness would have been nice.
- ckuehne 17y agoAs a starting point have a look at http://en.wikipedia.org/wiki/Predicate_transformer_semantics http://en.wikipedia.org/wiki/Predicate_transformer_semantics.
- gdp 17y agoAs has been said before, it's not about being "bug free" - it's about a number of safety properties always holding as long as the assumptions are true. The safety properties might be things like who can write to what memory, and when it is acceptable for bits of the kernel to do certain things. Lock freedom in scheduling is probably also a big thing. I haven't looked at any of this very closely, but I'm just guessing based on the sorts of properties I would try to prove initially.
- stcredzero 17y agoit's about a number of safety properties always holding as long as the assumptions are true And no project is ever without such assumptions. You can't have abstractions without them.
- gdp 17y agoI was using 'assumption' in the strict mathematical-logic sense. These assumptions are stated and it is trivial to check that the proof is not true if the assumptions aren't true.
- stcredzero 17y agoI was using 'assumption' to talk about the faith that abstractions and their (sometimes mathematical) assumptions can be successfully applied to solve real-world problems. Some may argue that there's no guarantee that such proofs apply to real world systems. But really, there's no guarantee that any abstract model does. We humans have to get paid for something.
- gdp 17y ago> Some may argue that there's no guarantee that such proofs apply to real world systems. I would argue that those who would argue that have probably not spent a lot of time doing any real-world formal verification. People seem to like arguing about its utility in the abstract without ever doing it.
- stcredzero 17y agoYou might be replying as if I'm disagreeing. If so, please re-read ancestor posts with the other spin. In short: most of the objections people have to formal verification also apply to modeling something in software to begin with.
- gdp 17y agoNo, I wasn't suggesting you were disagreeing, I was simply responding to your hypothetical disagreement that some might argue. My counter-argument could be just as applicable to any of the people who have professed similar beliefs to the ones you speculated that some may hold.
- stcredzero 17y agoIt's not so hypothetical. It's more the typical response of a programmer when formal methods come up. But I meant it as an observation of typical reactions, not as a hypothetical debate.