An example why verified programming is hard.

[hendrikboom]

Walking back from where I parked my car today, I realized how difficult it is to make sure specifications are satisfied, once you start looking at them formally. There are specifications with obvious meanings, and obvious algorithms to satisfy them. But

Comments

[sps]

I have to admit that my first reaction was "that's not a well-formed specification." It seems to make the global serialisation assumption, and that's not physics. Not unless there's a parking attendant....

[hendrikboom]

Well, duh. But we're both experienced software professionals, and global serialisation is the kind of abstract ideas we've learned to use to guide us away from traps -- the kind of concept that guides us when we design a system, whereas lesser, or less experienced, programmers try to patch up the problem during debugging.

[sps]

Well, duh, yes, but I think the question I completely failed to articulate was whether there's a distinction between a preformal/conceptual part that you need to get right (like, is 'now' a useful idea in this context?) and the formal component - or is it 'flat.' I tend to think of the plausibility of synchronisation as a matter of physics rather than one of computing, but I don't know if that's just me....