Timeline for Can a language be sound if it doesn't promise safety?
Current License: CC BY-SA 4.0
37 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 27 at 6:40 | history | protected | gnat | ||
| Aug 25 at 21:14 | history | edited | Ghassen | CC BY-SA 4.0 | added 1594 characters in body |
| Aug 22 at 19:34 | comment | added | Filip Milovanović | Yeah. On a more general note, this sort of terminological ambiguity happens in any field. Even in fields like math and physics, which are famous in popular perception for being exact/precise/strict, there are terms and notions that are related to the same basic idea, but have different precise meanings in different subfields or contexts (the differences are sometimes subtle, sometimes less so). Which is one of the reasons various technical publications have a section that defines terms - it's a way of saying "within this context, this is what these things mean". Just something to be aware of. | |
| Aug 22 at 19:14 | comment | added | Ghassen | @FilipMilovanović I think that's one of the key ideas I learned from this discussion, even though it feels difficult to find the "set of X"... it seems it's the thing that led to me getting confused by the definition. Programmers define that set based on what they think is right, like the example I wrote in my question.... I've heard so many say C is unsound because it allows out of bound access. Also, it seems many people think soundness = safety, and by "safety" they seem to mean it makes them feel safe or they don't feel it's reliable and could lead to disastrous errors. | |
| Aug 22 at 18:30 | comment | added | Filip Milovanović | These terms (soundness, completeness) are technical terms coming from the mathematical field of formal logic. There, these notions are not defined "with respect to X", but in general. In the particular formulation you have cited, these notions are defined w/ resp. to X, and by extension, w/ resp. to some collection of desirable X's (what the type system "promises" to prevent). So, when there are multiple notions of soundness, any claim about the soundness of a type system should come with an associated collection of X's that are being considered, otherwise any debate is pointless. | |
| Aug 21 at 1:50 | comment | added | Steve | @Caleth, I'm not saying they are "misused", but they are most often used in a manner that subverts what a compiler maker would regard as "sound typing" - which I associate with a practice by which types are always explicitly and accurately recorded in source code, and therefore type checking can be done mechanically by the compiler. Ritchie didn't intend C to have sound typing in the first place - the issue is not that reinterpret casts violate the promises of C, it's that C violates the promises of sound typing (which some people, though not Ritchie, say a programming language ought to have). | |
| Aug 20 at 11:15 | comment | added | Caleth | @Steve are you saying reinterpret casts are often misused, leading to undefined behaviour? Because C doesn't make any promises for all programs, only for well-formed ones. | |
| Aug 20 at 10:15 | comment | added | Steve | Btw to be clear, I'm playing devil's advocate here. I'm not saying that soundness comes across to me as making total sense, or that I think it is a desirable property of a language. I'm just trying to explain the line of thinking of those who advocate or use the concept. Whilst I guess it is possible for two distinct types to be wholly compatible, having a one-to-one bit representation of every state and the operations of either type being all fully valid, I would think that's the less common case where a reinterpret cast is actually used. (2/2) | |
| Aug 20 at 10:11 | comment | added | Steve | @Caleth, well there are usually specific conversion routines for ordinary casts. If these routines can throw a runtime error, then the type system is considered unsound - for a legitimate conversion to happen in a sound type system, every possible input to a conversion must map to a valid output (the rationale being: why would you write a program that accepts inputs that lead to crashes?). A reinterpreting cast will not throw, but as a result it typically allows some possible inputs to map to invalid outputs, thus violating the constraints which a sound type system would enforce. (1/2) | |
| Aug 20 at 8:01 | answer | added | Caleth | timeline score: 5 | |
| Aug 20 at 6:29 | comment | added | Caleth | @Steve how is that different from any other function from one type to another? | |
| Aug 19 at 20:23 | answer | added | gnasher729 | timeline score: 0 | |
| Aug 19 at 16:34 | answer | added | JacquesB | timeline score: 1 | |
| Aug 19 at 15:58 | comment | added | Greg Burghardt | More interesting results from DuckDuckGo: what is an unsound programming language | |
| Aug 19 at 15:57 | comment | added | Greg Burghardt | Related question in the Programming Language and Implementation community: What does it mean for a type system or language to be "sound"? I don't really know if it counts as a cross-site duplicate, but it does help set the context for this question. Maybe it helps? | |
| Aug 19 at 15:19 | comment | added | Doc Brown | @Ghassen: I took the freedom to improved the citing. I think without this cite, the question was quite unclear | |
| Aug 19 at 15:15 | history | edited | Doc Brown | CC BY-SA 4.0 | Citing improved |
| Aug 19 at 15:09 | answer | added | JonasH | timeline score: 2 | |
| Aug 19 at 15:02 | comment | added | Steve | @Caleth, yes, some other type which, according to the type system of that particular compiler, are not related or mutually assignable. | |
| Aug 19 at 12:07 | history | reopened | Steve Caleth Greg Burghardt | ||
| Aug 19 at 11:07 | comment | added | Caleth | @Steve reinterpret casts don't suggest that a variable has multiple types. It suggests that you can take the bit pattern corresponding to a value of one type, and get a value of some other type that corresponds to that bit pattern. | |
| Aug 19 at 10:56 | comment | added | Steve | The existence of reinterpreting casts, for example, breaks no guarantee in C, but it does suggest that the value in question either does not have a definite type, or that it has a definite type that at times is different from that recorded in source code. I think this is more of a concern for compiler writers and their optimising tricks or the pretenses of some about "correctness", than it is for programmers though. (2/2) | |
| Aug 19 at 10:56 | comment | added | Steve | The funniest thing about "type soundness" seems to be that nobody can agree on a definition of it that is sound! I don't think it's so much about "violating guarantees" (which as you observe, may or may not have been given), but about whether each value always has a definite type (as defined by that language) at a particular time, and this definite type can always be inferred by the compiler from the source code. (1/2) | |
| S Aug 19 at 10:02 | review | Reopen votes | |||
| Aug 19 at 12:19 | |||||
| S Aug 19 at 10:02 | history | edited | Ghassen | CC BY-SA 4.0 | added 558 characters in body Added to review |
| Aug 19 at 9:54 | comment | added | Ghassen | @tofro here is someone who claims it is unsound, although he mentions that soundness isn't a yes/no question, and he doesn't really care much about the academic definition of it. but I'm still trying to understand the topic, and haven't yet reached a conclusion. | |
| Aug 19 at 9:24 | history | removed from network questions | CPlus♦ | ||
| Aug 19 at 9:23 | history | closed | gnat Bart van Ingen Schenau CPlus♦ | Needs details or clarity | |
| Aug 19 at 8:50 | history | became hot network question | |||
| Aug 19 at 8:18 | comment | added | Caleth | "We expect the expression medicineAmounts[i] to always evaluate to a value of type float (which it does—the garbage values are still bit patterns interpreted as floats)." No, the program has undefined behaviour. The rest of the rules of C don't apply and the implementation can do whatever it wants. E.g. a compiler can assume this is unreachable code and omit it. | |
| Aug 19 at 7:30 | comment | added | tofro | .... and I never heard anyone say "C is unsound" - please give a reference. C is GIGO (and very educational ...) - do you mean the same thing? | |
| Aug 19 at 7:26 | comment | added | tofro | Your assumption "which it does - ...." is wrong. OOB access is UB, and UB means "you can't assume anything", as you rightly say. OOB access out of an allocated page willl not be interpreted as a float. | |
| Aug 19 at 6:53 | answer | added | guest271314 | timeline score: -1 | |
| Aug 19 at 6:02 | review | Close votes | |||
| Aug 19 at 9:23 | |||||
| Aug 18 at 23:54 | comment | added | CPlus♦ | A language is only as unsound to the extent that the programmer does unsupported things. | |
| Aug 18 at 23:48 | answer | added | Christophe | timeline score: 2 | |
| Aug 18 at 22:10 | history | asked | Ghassen | CC BY-SA 4.0 |