6 ms·

Looks like the requirements for a "type system" have increased since I last looked - according to the article, a type system only deserves that name if it preve

by rob74 3y ago

Looks like the requirements for a "type system" have increased since I last looked - according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. And here was I thinking that every strongly typed language already has a type system (a more or less sound one, but a type system)? Ok, TBF they mention that they are using a "fairly narrow" (re)definition of the term...

avgcorrection 3y ago
There’s a difference between a type system and a type system that is sound. > according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. Soundness is a technical term. Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior. Imagine if a logician said the following: - Here is my sound and complete logic - By the way, some valid formulas will give you Undefined Behavior and I don’t care what happens in those cases That would be pretty wild.
- DaiPlusPlus 3y ago
  > Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior UB in C allows for a lot more than just memory corruption though (c.f.: nasal demons). Also, what about alternatives to UB, such as requiring a compiler error and/or runtime fatal error?
  - stonemetal12 3y ago
    If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.
mrkeen 3y ago
> a type system only deserves that name if it prevents use-after-free errors Or another way to look at it: if I tell you you're holding an Integer, and when you try to use it in addition, it explodes, was I really justified in telling you you were holding an Integer?
- rwmj 3y ago
  That's kind of a bad example because adding integers can overflow (in some languages).
  - shadowgovt 3y ago
    Depending on how you turn your head and squint, overflow is still well-defined: if I add a to b and it overflows to c, it still overflows to the same c every time. That means addition is sound in that architecture, it just has surprising consequences and some properties one would expect naively to hold for positive-integer arithmetic don't hold for the computer addition operation (such as c > a && c > b for all a > 0 and b > 0).
    - staunton 3y ago
      C/C++ (the standard) makes no claims about what happens if you overflow integers. The program might set all your variables in the whole program to zero if it likes. Of course the compiler vendors wouldn't do that but they're allowed to. That's what "undefined" means at least in C/C++.
      - Kamq 3y ago
        > C/C++ (the standard) makes no claims about what happens if you overflow integers. It makes no claims on what happens when you overflow signed integers. Unsigned integer wrapping is specified by section 6.2.5, paragraph 9 of the C standard.
cvoss 3y ago
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. I mean, you are hiding a lot of possibilities in "etc. etc.". So is the article, when it says "and the like" in the sentence you're referring to. The kinds of things that belong in this list are described as "generally some sort of safety property." That's a big big list of things. It's not a particularly strict or narrow definition of type system, IMO. Take C. What does it mean when C's type system says a variable "x" has type "int"? Practically, it means the compiler knows how many bytes (let's say 4) to reserve on the stack for x. But what if the program, during the course of execution, tries to write an 8-byte piece of data to x? The language is broken if that can occur because the compiler was not justified in reserving only 4 bytes for x. So, part and parcel of C's type system is a global safety property: It promises, among many other things, that at runtime no assignment will ever occur to an int-typed variable unless the assignment payload is 4 bytes. So this is exactly what the article is talking about. Local rules (e.g., "int x = y" is well-typed if y has type int) working together to guarantee a global safety property (no type mismatches can occur at runtime). The failure of a type system to do this properly is a failure at being a type system. And indeed, since C has undefined behavior, it's type system falls apart immediately. It's just not even interesting to consider enumerating the ways it can be broken. The type systems considered by this article are ostensibly supposed to not be broken the way C's is. That's what makes the counterexamples of this article so interesting.
Sharlin 3y ago
From the specific perspective of the article, C++’s type system is uninteresting because it’s so trivially and fundamentally unsound. It’s easy to come up with a single line of C++ (eg. overflowing a signed int) that works as a counterexample. Languages whose type systems make stronger guarantees you have to make an effort to break. A type system that allows undefined behavior is equivalent to a logic system that allows proving a falsehood, and ex falso quodlibet – from a falsehood you can prove anything.
kccqzy 3y ago
> more or less sound There isn't more or less sound. There's really only sound or not.
- AnimalMuppet 3y ago
  Then there's really only "not". If you require perfect, 100% soundness in all circumstances, then nothing is sound. (Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.) If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.
  - salawat 3y ago
    >If you require perfect, 100% soundness in all circumstances, then nothing is sound. Soundness in logic requires both valid form, and reasoning from true premises.
    - staunton 3y ago
      The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".
- staunton 3y ago
  We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never prove 100% what any given program will do on a computer. Indeed, it's impossible to prove absolutely any fact about a real physical system. You prove things about abstract mathematical objects. Such a proof may be useful in practice when the assumptions you made for the proof are satisfied to a sufficient degree in a sufficient number of cases. Whether this is the case or not is ultimately a matter of judgement (and data, for which you have to use judgement in collecting/interpreting it, and data, for which...) By the way, the paper you're using to write proofs in mathematical logic is a physical system.
lmm 3y ago
What does it even mean for a program to be well-typed if that program has "use-after-free errors, memory corruption etc. etc."? A program with C-style undefined behaviour could ipso facto fail with a type error on any given line.
kelnos 3y ago
You are conflating two different (but related) concepts. The requirements for type system to be a type system have not changed. Neither have the requirements for soundness. Most mainstream languages have tacitly accepted unsoundness for decades, but newer languages aim to have type systems with fewer and fewer unsound rough edges. For example, I would consider Java to be a strongly-typed language, but it has quite a few unsoundness issues that can come up in regular, non-contrived code. Scala's type system is stronger and more full-featured, but it's not clear to me that it's significantly more sound. Rust, perhaps, has a (strong) type system with fewer soundness issues than both Java and Scala, but some issues do exist. C and C++ have comparatively weak type systems (though C++'s is certainly stronger than C's), and their type systems have quite a few soundness issues, many of which that can be exposed via simple one-liners. Also consider that soundness issues are not all created equal. I would much rather see a ClassCastException at runtime in a Java or Scala program, than see memory corruption (with possible security or data-integrity consequences) in a "valid" C/C++ program when I misuse memory designated as one type, as another. Certainly the best case would be a compiler that wouldn't allow it in the first place, but the Java/Scala example is nowhere near as bad as the C/C++ example.

by rob74 3y ago

avgcorrection 3y ago

There’s a difference between a type system and a type system that is sound. > according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. Soundness is a technical term. Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior. Imagine if a logician said the following: - Here is my sound and complete logic - By the way, some valid formulas will give you Undefined Behavior and I don’t care what happens in those cases That would be pretty wild.

DaiPlusPlus 3y ago
> Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior UB in C allows for a lot more than just memory corruption though (c.f.: nasal demons). Also, what about alternatives to UB, such as requiring a compiler error and/or runtime fatal error?
- stonemetal12 3y ago
  If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.

mrkeen 3y ago

> a type system only deserves that name if it prevents use-after-free errors Or another way to look at it: if I tell you you're holding an Integer, and when you try to use it in addition, it explodes, was I really justified in telling you you were holding an Integer?

rwmj 3y ago
That's kind of a bad example because adding integers can overflow (in some languages).
- shadowgovt 3y ago
  Depending on how you turn your head and squint, overflow is still well-defined: if I add a to b and it overflows to c, it still overflows to the same c every time. That means addition is sound in that architecture, it just has surprising consequences and some properties one would expect naively to hold for positive-integer arithmetic don't hold for the computer addition operation (such as c > a && c > b for all a > 0 and b > 0).
  - staunton 3y ago
    C/C++ (the standard) makes no claims about what happens if you overflow integers. The program might set all your variables in the whole program to zero if it likes. Of course the compiler vendors wouldn't do that but they're allowed to. That's what "undefined" means at least in C/C++.
    - Kamq 3y ago
      > C/C++ (the standard) makes no claims about what happens if you overflow integers. It makes no claims on what happens when you overflow signed integers. Unsigned integer wrapping is specified by section 6.2.5, paragraph 9 of the C standard.

cvoss 3y ago

> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. I mean, you are hiding a lot of possibilities in "etc. etc.". So is the article, when it says "and the like" in the sentence you're referring to. The kinds of things that belong in this list are described as "generally some sort of safety property." That's a big big list of things. It's not a particularly strict or narrow definition of type system, IMO. Take C. What does it mean when C's type system says a variable "x" has type "int"? Practically, it means the compiler knows how many bytes (let's say 4) to reserve on the stack for x. But what if the program, during the course of execution, tries to write an 8-byte piece of data to x? The language is broken if that can occur because the compiler was not justified in reserving only 4 bytes for x. So, part and parcel of C's type system is a global safety property: It promises, among many other things, that at runtime no assignment will ever occur to an int-typed variable unless the assignment payload is 4 bytes. So this is exactly what the article is talking about. Local rules (e.g., "int x = y" is well-typed if y has type int) working together to guarantee a global safety property (no type mismatches can occur at runtime). The failure of a type system to do this properly is a failure at being a type system. And indeed, since C has undefined behavior, it's type system falls apart immediately. It's just not even interesting to consider enumerating the ways it can be broken. The type systems considered by this article are ostensibly supposed to not be broken the way C's is. That's what makes the counterexamples of this article so interesting.

Sharlin 3y ago

From the specific perspective of the article, C++’s type system is uninteresting because it’s so trivially and fundamentally unsound. It’s easy to come up with a single line of C++ (eg. overflowing a signed int) that works as a counterexample. Languages whose type systems make stronger guarantees you have to make an effort to break. A type system that allows undefined behavior is equivalent to a logic system that allows proving a falsehood, and ex falso quodlibet – from a falsehood you can prove anything.

kccqzy 3y ago

> more or less sound There isn't more or less sound. There's really only sound or not.

AnimalMuppet 3y ago
Then there's really only "not". If you require perfect, 100% soundness in all circumstances, then nothing is sound. (Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.) If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.
- salawat 3y ago
  >If you require perfect, 100% soundness in all circumstances, then nothing is sound. Soundness in logic requires both valid form, and reasoning from true premises.
  - staunton 3y ago
    The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".
staunton 3y ago
We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never prove 100% what any given program will do on a computer. Indeed, it's impossible to prove absolutely any fact about a real physical system. You prove things about abstract mathematical objects. Such a proof may be useful in practice when the assumptions you made for the proof are satisfied to a sufficient degree in a sufficient number of cases. Whether this is the case or not is ultimately a matter of judgement (and data, for which you have to use judgement in collecting/interpreting it, and data, for which...) By the way, the paper you're using to write proofs in mathematical logic is a physical system.

lmm 3y ago

What does it even mean for a program to be well-typed if that program has "use-after-free errors, memory corruption etc. etc."? A program with C-style undefined behaviour could ipso facto fail with a type error on any given line.

kelnos 3y ago

You are conflating two different (but related) concepts. The requirements for type system to be a type system have not changed. Neither have the requirements for soundness. Most mainstream languages have tacitly accepted unsoundness for decades, but newer languages aim to have type systems with fewer and fewer unsound rough edges. For example, I would consider Java to be a strongly-typed language, but it has quite a few unsoundness issues that can come up in regular, non-contrived code. Scala's type system is stronger and more full-featured, but it's not clear to me that it's significantly more sound. Rust, perhaps, has a (strong) type system with fewer soundness issues than both Java and Scala, but some issues do exist. C and C++ have comparatively weak type systems (though C++'s is certainly stronger than C's), and their type systems have quite a few soundness issues, many of which that can be exposed via simple one-liners. Also consider that soundness issues are not all created equal. I would much rather see a ClassCastException at runtime in a Java or Scala program, than see memory corruption (with possible security or data-integrity consequences) in a "valid" C/C++ program when I misuse memory designated as one type, as another. Certainly the best case would be a compiler that wouldn't allow it in the first place, but the Java/Scala example is nowhere near as bad as the C/C++ example.