17 ms·

I've worked a lot with TypeScript after a background in more type-y languages like O'Caml and Haskell and have eventually gained a real appreciation for the eng

by evmar 9y ago

I've worked a lot with TypeScript after a background in more type-y languages like O'Caml and Haskell and have eventually gained a real appreciation for the engineering tradeoff they made. This article sorta frames soundness like it's a feature -- one could have soundness or not, so why not have it -- when in really a specific technical term about a property of a language that programmers often don't understand (as evidenced by the other comments on here) and which has specific consequences. Instead, I now view type systems as a tool that can make tradeoffs to get the job done, in the same space as "IDE" or "test-driven design". With those it's easy to make statements about the specific programmer tradeoffs, such as "test-driven design means you spend more time writing tests but gives you more confidence about the results". With a given type system, you can evaluate it like "type system X lets you get autocomplete in your editor", or "type system Y catches the common error of Z". Meanwhile if you only focus on soundness you end up with counterintuitive results like where Java is sound but still has NullPointerExceptions everywhere, or languages like Rust where whole data structures and algorithms are disallowed because you can't express their correctness to the compiler. (To be clear I appreciate exactly why Rust must do this, but again you can evaluate that tradeoff as "preserves memory safety without GC, disallows doubly-linked lists" rather than "is the type system 'correct'".) One view that really opened my eyes on this Gilad Bracha's talk on pluggable and optional type systems: http://lambda-the-ultimate.org/node/1311 http://lambda-the-ultimate.org/node/1311 .

yawaramin 9y ago
Soundness really shouldn't be up for trade-off. If you can't even trust that your static types will be the same as the run-time types, what even is the point of having types? Btw, Java is unsound; see 'Java and Scala's Type Systems are Unsound - Semantic Scholar' ( https://pdfs.semanticscholar.org/3705/c660290e98877f882cf908ed253a36c5e508.pdf https://pdfs.semanticscholar.org/3705/c660290e98877f882cf908... )
- seanmcdirmid 9y ago
  Soundness is a trade-off. If you can have static types that work for a lot of the Javascript already out there without soundness or no types at all, which one do you pick? Type system traditionalists think that static typing is all just about universal type checking, they ignore development tools, code completion, or useful but not absolute best effort type checking. Programming in Typescript really is nice because the type system helps even if it isn't perfect. It shows that there is a lot in the design space between "no static typing" and "sound static typing". Evidence Java and Scala being widely used even if they are technically unsound (where soundness itself is really a gradient). Type systems simply aren't black and white as the fundamentalists would claim.
  - yawaramin 9y ago
    > If you can have static types that work for a lot of the Javascript already out there without soundness or no types at all, which one do you pick? You restrict the allowable subset of JavaScript in your codebase further to one you know is sound. This is pretty much the same strategy that `"use strict"` has, and literally no one complains about that, so it was never really about restricting JavaScript anyway, people just like to dump on soundness as being too un-pragmatic. Sure, sometimes you really do need to work around the type system and express something you know can't go wrong. But it's always possible to contain it to a small, 'unsafe' part of the codebase! For example, Rust proves this quite nicely.
    - foldr 9y ago
      A major design goal of TypeScript is to make it as easy as possible to annotate existing JavasScript code bases with types. >But it's always possible to contain it to a small, 'unsafe' part of the codebase! It's not "contained" when it comes to soundness. Unsafe Rust code could perfectly well screw up invariants that are required for soundness.
      - Jweb_Guru 9y ago
        However, if the unsafe code is written correctly, it is in fact well encapsulated. We can prove this now, it's no longer just conjecture.
        foldr 9y ago
        If the unsafe code is written "correctly" then of course, by definition, there isn't anything to worry about. The same is true of unsafe code in C or assembly. I took a look at the paper that you're obliquely referring to [1], and I think you are exaggerating the significance of its results for practical Rust programming. In fact, the paper underlines how difficult it is to use 'unsafe' correctly. As soon as you use any unsafe code, the language can no longer guarantee that any of your code is safe. Thus, to guarantee safety, you must either never use unsafe code except in libraries which have already been proven safe, or develop proofs for your own unsafe code. There are many instances where it is almost mandatory to use unsafe code in Rust (e.g. writing a mutable iterator for a custom data structure), so this is not a theoretical problem. As far as provable safety is concerned, the situation seems pretty similar to the situation in C++ (for which there is already a vast literature on techniques for formal verification of safety). That is not to deny that Rust code is likely to be safer than C++ code in practice. However, that has nothing to do with having unsafe operations block-scoped and tagged with the 'unsafe' keyword. I'm not a fan of this syntax because it can easily give newcomers to the language the mistaken impression that the danger is somehow contained within the relevant block. [1] http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202.pdf?ip=88.98.193.174&id=3158154&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EC1E31BC46E58D5B8&__acm__=1523184964_df705dd5d3b548febf25f0e2b505a5c8 http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202....
tel 9y ago
Java isn't sound and the poor semantics of null are critical to proving it. Not that this takes away from your larger point exactly, but Java+null is no longer a good example.
- evmar 9y ago
  As I was saying in the comment, Java is sound* by their definition of what soundness means, and it is exactly why it's a great example. You probably have some intuition about some desired property you have (like "doesn't crash/throw at runtime"), but that is a different property than soundness. You can certainly evaluate a type system against that property as well. But a type system that completely proves a program does not crash at runtime must be able to e.g. prove that it never runs out of memory, that recursive functions terminate, and the resulting allowable programs cannot do very much. * It turns out Java accidentally turned out to be unsound in a really obscure corner case, unrelated to the nulls thing. https://hackernoon.com/java-is-unsound-28c84cb2b3f https://hackernoon.com/java-is-unsound-28c84cb2b3f
  - leshow 9y ago
    You seem to be including the halting problem in your definition of type soundness, those aren't the same things. Java has always had covariant arrays, which are not sound. Whether it was intentional or not is irrelevant to the question of 'does this language have a sound type system?'.
    - evmar 9y ago
      I agree that termination isn't part of soundness. I was trying to explain how null pointer exceptions are compatible with soundness in Java. As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?
      - leshow 9y ago
        Perhaps you're right there since the check is moved to runtime, I must have glossed over that. If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.
jjnoakes 9y ago
> whole data structures and algorithms are disallowed Nothing is disallowed in rust. You may need a specialized crate or a small 'unsafe' block to work beyond the compiler's ability to prove your code meets rust's guarantees, but that's not the same as inexpressible.
- quotemstr 9y ago
  Unsafe rust is a superset of safe Rust. They're two different languages. The OP is saying, correctly, that certain data structures are inexpressible in safe Rust. That's fine. Certain control flow structures are inexpressible in goto-less C.
  - jjnoakes 9y ago
    > The OP is saying, correctly, that certain data structures are inexpressible in safe Rust The op didn't say "safe rust", that's my point.
  - irundebian 9y ago
    > Certain control flow structures are inexpressible in goto-less C. I'm not sure about that. C contains while loops. And every GOTO-computable programs should be expressible by WHILE-computable programs. See (slide 21): http://ai.cs.unibas.ch/_files/teaching/fs16/theo/slides/theory-d03.pdf http://ai.cs.unibas.ch/_files/teaching/fs16/theo/slides/theo...
    - stormbrew 9y ago
      I don't think "certain control flow structures are inexpressible" is the same assertion as "certain programs are unexpressible"... After all, any turing complete system will have a similar set of computable programs as another, but they will not all have the same control structures. For example, you can have a turing complete language with no loops, only recursion. Both can express the same programs but not in the same way. That said, it's also a bit of a tautology so.
- Too 9y ago

by evmar 9y ago

yawaramin 9y ago

Soundness really shouldn't be up for trade-off. If you can't even trust that your static types will be the same as the run-time types, what even is the point of having types? Btw, Java is unsound; see 'Java and Scala's Type Systems are Unsound - Semantic Scholar' ( https://pdfs.semanticscholar.org/3705/c660290e98877f882cf908ed253a36c5e508.pdf https://pdfs.semanticscholar.org/3705/c660290e98877f882cf908... )

seanmcdirmid 9y ago
Soundness is a trade-off. If you can have static types that work for a lot of the Javascript already out there without soundness or no types at all, which one do you pick? Type system traditionalists think that static typing is all just about universal type checking, they ignore development tools, code completion, or useful but not absolute best effort type checking. Programming in Typescript really is nice because the type system helps even if it isn't perfect. It shows that there is a lot in the design space between "no static typing" and "sound static typing". Evidence Java and Scala being widely used even if they are technically unsound (where soundness itself is really a gradient). Type systems simply aren't black and white as the fundamentalists would claim.
- yawaramin 9y ago
  > If you can have static types that work for a lot of the Javascript already out there without soundness or no types at all, which one do you pick? You restrict the allowable subset of JavaScript in your codebase further to one you know is sound. This is pretty much the same strategy that `"use strict"` has, and literally no one complains about that, so it was never really about restricting JavaScript anyway, people just like to dump on soundness as being too un-pragmatic. Sure, sometimes you really do need to work around the type system and express something you know can't go wrong. But it's always possible to contain it to a small, 'unsafe' part of the codebase! For example, Rust proves this quite nicely.
  - foldr 9y ago
    A major design goal of TypeScript is to make it as easy as possible to annotate existing JavasScript code bases with types. >But it's always possible to contain it to a small, 'unsafe' part of the codebase! It's not "contained" when it comes to soundness. Unsafe Rust code could perfectly well screw up invariants that are required for soundness.
    - Jweb_Guru 9y ago
      However, if the unsafe code is written correctly, it is in fact well encapsulated. We can prove this now, it's no longer just conjecture.
      - foldr 9y ago
        If the unsafe code is written "correctly" then of course, by definition, there isn't anything to worry about. The same is true of unsafe code in C or assembly. I took a look at the paper that you're obliquely referring to [1], and I think you are exaggerating the significance of its results for practical Rust programming. In fact, the paper underlines how difficult it is to use 'unsafe' correctly. As soon as you use any unsafe code, the language can no longer guarantee that any of your code is safe. Thus, to guarantee safety, you must either never use unsafe code except in libraries which have already been proven safe, or develop proofs for your own unsafe code. There are many instances where it is almost mandatory to use unsafe code in Rust (e.g. writing a mutable iterator for a custom data structure), so this is not a theoretical problem. As far as provable safety is concerned, the situation seems pretty similar to the situation in C++ (for which there is already a vast literature on techniques for formal verification of safety). That is not to deny that Rust code is likely to be safer than C++ code in practice. However, that has nothing to do with having unsafe operations block-scoped and tagged with the 'unsafe' keyword. I'm not a fan of this syntax because it can easily give newcomers to the language the mistaken impression that the danger is somehow contained within the relevant block. [1] http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202.pdf?ip=88.98.193.174&id=3158154&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EC1E31BC46E58D5B8&__acm__=1523184964_df705dd5d3b548febf25f0e2b505a5c8 http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202....

tel 9y ago

Java isn't sound and the poor semantics of null are critical to proving it. Not that this takes away from your larger point exactly, but Java+null is no longer a good example.

evmar 9y ago
As I was saying in the comment, Java is sound* by their definition of what soundness means, and it is exactly why it's a great example. You probably have some intuition about some desired property you have (like "doesn't crash/throw at runtime"), but that is a different property than soundness. You can certainly evaluate a type system against that property as well. But a type system that completely proves a program does not crash at runtime must be able to e.g. prove that it never runs out of memory, that recursive functions terminate, and the resulting allowable programs cannot do very much. * It turns out Java accidentally turned out to be unsound in a really obscure corner case, unrelated to the nulls thing. https://hackernoon.com/java-is-unsound-28c84cb2b3f https://hackernoon.com/java-is-unsound-28c84cb2b3f
- leshow 9y ago
  You seem to be including the halting problem in your definition of type soundness, those aren't the same things. Java has always had covariant arrays, which are not sound. Whether it was intentional or not is irrelevant to the question of 'does this language have a sound type system?'.
  - evmar 9y ago
    I agree that termination isn't part of soundness. I was trying to explain how null pointer exceptions are compatible with soundness in Java. As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?
    - leshow 9y ago
      Perhaps you're right there since the check is moved to runtime, I must have glossed over that. If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.

jjnoakes 9y ago

> whole data structures and algorithms are disallowed Nothing is disallowed in rust. You may need a specialized crate or a small 'unsafe' block to work beyond the compiler's ability to prove your code meets rust's guarantees, but that's not the same as inexpressible.

quotemstr 9y ago
Unsafe rust is a superset of safe Rust. They're two different languages. The OP is saying, correctly, that certain data structures are inexpressible in safe Rust. That's fine. Certain control flow structures are inexpressible in goto-less C.
- jjnoakes 9y ago
  > The OP is saying, correctly, that certain data structures are inexpressible in safe Rust The op didn't say "safe rust", that's my point.
- irundebian 9y ago
  > Certain control flow structures are inexpressible in goto-less C. I'm not sure about that. C contains while loops. And every GOTO-computable programs should be expressible by WHILE-computable programs. See (slide 21): http://ai.cs.unibas.ch/_files/teaching/fs16/theo/slides/theory-d03.pdf http://ai.cs.unibas.ch/_files/teaching/fs16/theo/slides/theo...
  - stormbrew 9y ago
    I don't think "certain control flow structures are inexpressible" is the same assertion as "certain programs are unexpressible"... After all, any turing complete system will have a similar set of computable programs as another, but they will not all have the same control structures. For example, you can have a turing complete language with no loops, only recursion. Both can express the same programs but not in the same way. That said, it's also a bit of a tautology so.
Too 9y ago