3 ms·
Formally, "safety" = "preservation" + "progress". So, using those loose definitions together doesn't fit what I'm referring to. In particular, "does not access
by tel 12y ago
Formally, "safety" = "preservation" + "progress". So, using those loose definitions together doesn't fit what I'm referring to.
In particular, "does not access elements outside of the bounds of the array" is not directly a safety property, though it could be interpreted within the dynamics in order to ensure progress. For instance, if you outlaw exception throwing then the types must ensure that exceptional states cannot arise. Else the program can "get stuck" and progress is refuted.
The final point about sorted arrays again mistakes putting "safety" and "progress" on the same epistemological ground.
- mcguire 12y agoHm. I had never heard of "preservation" as a category in itself, other than as a synonym for safety. But I come from a distributed systems/network protocol background, many years ago, so all of the landmarks have moved. Not sure what the distinction buys you, though.
- tel 12y agoIt gives you the proof that's loosely stated as "well-types programs do not go wrong". The sketch is that if some thing is well-typed then progress means it won't "go wrong" and preservation means it'll stay well-typed. Thus: well-typed programs progress all the way to stable values.