3 ms·

Why do these sorts of articles always give vague definitions of Soundness and act like it exists on a spectrum? Soundness = Progress & Preservation. From Pier

Why do these sorts of articles always give vague definitions of Soundness and act like it exists on a spectrum? Soundness = Progress & Preservation. From Pierce's Types And Programming Languages: "Progress: A well typed term is not stuck (either it is a value or it can take a step according to the evaluation rules). Preservation: If a well typed term takes a step of evaluation, then the resulting term is well typed." There are not degrees to Soundness and it is a well defined term.

gjm11 7y ago
You've shown that one can give a black-and-white definition of soundness and have it be useful. That doesn't mean that there's no way to give useful meaning to "more sound" or "less sound". Consider the following family of languages: L has a sound type system. LD (D for "dynamic") is L plus the ability to escape from it, in specially marked "unsafe" sections of code, into a dynamically typed system. (So evaluation can produce runtime errors, but they can be handled safely.) LC (C for "crash") is L plus the ability to escape in "unsafe" sections into a system like Ld's except that now type errors aren't checked for and caught at runtime, they just produce memory-stomping and buffer overflows and the like. D is just LD's "unsafe" language. C is just LD's "unsafe" language. (Any resemblance to actual real-world languages named C, living or dead, is purely coincidental.) The only one of these languages that is sound is L, of course. But there is some quality closely related to soundness by which there's an obvious partial ordering where L > LD > D, L > LC > C, LD > LC, and D > C, and if someone describes this situation by saying that LD is "sounder" than C then I don't see any reason why we should stop them. Similarly: a federal state is either a "perfect union" or not, for any reasonable definition of "perfect", but it's reasonable for the US constitution to aim at a "more perfect union". A thing is either "unique" or not, but despite the cries of pedants it's reasonable to describe a limited-edition Ferrari of which only two were ever made as "almost unique" and as "more unique" than a standard-issue Ford Fiesta. A given region of space is either "vacuum" or not, but most of the things we describe as "vacuum" actually contain some very rarefied gas and it's common to use terms like "high vacuum" to quantify how vacuum-like a "vacuum" is.

gjm11 7y ago

You've shown that one can give a black-and-white definition of soundness and have it be useful. That doesn't mean that there's no way to give useful meaning to "more sound" or "less sound". Consider the following family of languages: L has a sound type system. LD (D for "dynamic") is L plus the ability to escape from it, in specially marked "unsafe" sections of code, into a dynamically typed system. (So evaluation can produce runtime errors, but they can be handled safely.) LC (C for "crash") is L plus the ability to escape in "unsafe" sections into a system like Ld's except that now type errors aren't checked for and caught at runtime, they just produce memory-stomping and buffer overflows and the like. D is just LD's "unsafe" language. C is just LD's "unsafe" language. (Any resemblance to actual real-world languages named C, living or dead, is purely coincidental.) The only one of these languages that is sound is L, of course. But there is some quality closely related to soundness by which there's an obvious partial ordering where L > LD > D, L > LC > C, LD > LC, and D > C, and if someone describes this situation by saying that LD is "sounder" than C then I don't see any reason why we should stop them. Similarly: a federal state is either a "perfect union" or not, for any reasonable definition of "perfect", but it's reasonable for the US constitution to aim at a "more perfect union". A thing is either "unique" or not, but despite the cries of pedants it's reasonable to describe a limited-edition Ferrari of which only two were ever made as "almost unique" and as "more unique" than a standard-issue Ford Fiesta. A given region of space is either "vacuum" or not, but most of the things we describe as "vacuum" actually contain some very rarefied gas and it's common to use terms like "high vacuum" to quantify how vacuum-like a "vacuum" is.