6 ms·

> 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 restric

> 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....
    - flurrything 9y ago
      That link is broken, but if it's the paper I think it is, the key result is that you can extend safe Rust with safe components that do use `unsafe` as long as you are able to prove these components to be sound. The same is not true of neither C nor assembly, and there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound. With safe Rust + the standard library there are almost no data-structures that you can't write.
      - foldr 9y ago
        >The same is not true of neither C nor assembly I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. > there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound Only if 'most' means 'all'! The paper itself notes that "...the problem cannot easily be contained by blessing a fixed set of standard libraries as primitive and just verifying the soundness of those; for although it is considered a badge of honor for Rust programmers to avoid the use of unsafe code entirely, many nevertheless find it necessary to employ a sprinkling of unsafe code in their developments." Non-broken link: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
        Jweb_Guru 9y ago
        > I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? What isn't possible is encapsulating many of the safe APIs that Rust supports using C's type system. You can restrict all of the C code in a program to a subset that is safe, but it isn't a subset that anyone actually uses; by contrast, it is absolutely feasible to write programs that use safe Rust outside a handful of unsafe functions in the standard library. The primary reason is that Rust's type system is capable of encapsulating many more safe guarantees than C's is. As someone who works on the RustBelt team, you are misunderstanding the paper. What the paper is arguing is that we need to be able to prove modularity for arbitrary unsafe code, not just treat the standard library as type system primitives, because we want Rust's set of "primitives" to be easily extensible. > The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. It is fundamentally different. C++ does not have lifetimes or compile time verification of ownership; its references cannot be safely encapsulated behind an API, and it does not have "modes" like share and own. These are all critical for Rust's safety proofs. This is not for lack of trying; many people have attempted to define safe subsets of C or C++, or add these features to C, such as Cyclone. In all cases, new concepts and types needed to be added to the language and most existing code was no longer usable.
seanmcdirmid 9y ago
Soundness can be too restrictive, there are a lot of useful things you can do in TypeScript even for new code bases that are not sound; e.g., you can re-apply an interface to any object even if it is impossible to know if the terms line up. After having used TypeScript for a year, it isn't a big deal, the type errors that might arise during debugging are never very surprising and usually related to logic probelms (I would have had those errors in C# because I would had to used weaker types anyways). I appreciate soundness, I've used sound languages, but I really dislike overly strict interpretations of soundness that dump on common constructs like null. Ya, null has some bad points, it will cause run-time exceptions, but so do many other things in a programming language. Yes, that level of soundness is way too un-pragmatic *for my needs. I understand the academic problems and I'm not losing any sleep over it. > 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. You can't isolate unsafe operations from only having isolated effects to the block of code flagged.
- steveklabnik 9y ago
  > You can't isolate unsafe operations from only having isolated effects to the block of code flagged. That's because the module is the isolation boundary in Rust, generally. So for maximum safety, getting the unsafe code into a smaller module and then re-exporting only its safe interface is the way to go.
  - foldr 9y ago
    Can't unsafe rust code convert integers to pointers and thus write to arbitrary memory locations within the address space of the process? The module boundary won't help with soundness, strictly speaking. If any unsafe code executes ever, then in principle it can (e.g.) zero out a pointer in some safe code which is guaranteed to be non-null as far as Rust is concerned.
    - Jweb_Guru 9y ago
      The point is that if the unsafe code is correct, any assumptions it is making need to be in the module. Ergo, you should only have to scan the module itself to figure out whether the code is unsafe or not, because if you can't prove safeness by looking at the module it's ipso facto not safe.

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....
  - flurrything 9y ago
    That link is broken, but if it's the paper I think it is, the key result is that you can extend safe Rust with safe components that do use `unsafe` as long as you are able to prove these components to be sound. The same is not true of neither C nor assembly, and there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound. With safe Rust + the standard library there are almost no data-structures that you can't write.
    - foldr 9y ago
      >The same is not true of neither C nor assembly I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. > there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound Only if 'most' means 'all'! The paper itself notes that "...the problem cannot easily be contained by blessing a fixed set of standard libraries as primitive and just verifying the soundness of those; for although it is considered a badge of honor for Rust programmers to avoid the use of unsafe code entirely, many nevertheless find it necessary to employ a sprinkling of unsafe code in their developments." Non-broken link: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      - Jweb_Guru 9y ago
        > I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? What isn't possible is encapsulating many of the safe APIs that Rust supports using C's type system. You can restrict all of the C code in a program to a subset that is safe, but it isn't a subset that anyone actually uses; by contrast, it is absolutely feasible to write programs that use safe Rust outside a handful of unsafe functions in the standard library. The primary reason is that Rust's type system is capable of encapsulating many more safe guarantees than C's is. As someone who works on the RustBelt team, you are misunderstanding the paper. What the paper is arguing is that we need to be able to prove modularity for arbitrary unsafe code, not just treat the standard library as type system primitives, because we want Rust's set of "primitives" to be easily extensible. > The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. It is fundamentally different. C++ does not have lifetimes or compile time verification of ownership; its references cannot be safely encapsulated behind an API, and it does not have "modes" like share and own. These are all critical for Rust's safety proofs. This is not for lack of trying; many people have attempted to define safe subsets of C or C++, or add these features to C, such as Cyclone. In all cases, new concepts and types needed to be added to the language and most existing code was no longer usable.

seanmcdirmid 9y ago

Soundness can be too restrictive, there are a lot of useful things you can do in TypeScript even for new code bases that are not sound; e.g., you can re-apply an interface to any object even if it is impossible to know if the terms line up. After having used TypeScript for a year, it isn't a big deal, the type errors that might arise during debugging are never very surprising and usually related to logic probelms (I would have had those errors in C# because I would had to used weaker types anyways). I appreciate soundness, I've used sound languages, but I really dislike overly strict interpretations of soundness that dump on common constructs like null. Ya, null has some bad points, it will cause run-time exceptions, but so do many other things in a programming language. Yes, that level of soundness is way too un-pragmatic *for my needs. I understand the academic problems and I'm not losing any sleep over it. > 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. You can't isolate unsafe operations from only having isolated effects to the block of code flagged.

steveklabnik 9y ago
> You can't isolate unsafe operations from only having isolated effects to the block of code flagged. That's because the module is the isolation boundary in Rust, generally. So for maximum safety, getting the unsafe code into a smaller module and then re-exporting only its safe interface is the way to go.
- foldr 9y ago
  Can't unsafe rust code convert integers to pointers and thus write to arbitrary memory locations within the address space of the process? The module boundary won't help with soundness, strictly speaking. If any unsafe code executes ever, then in principle it can (e.g.) zero out a pointer in some safe code which is guaranteed to be non-null as far as Rust is concerned.
  - Jweb_Guru 9y ago
    The point is that if the unsafe code is correct, any assumptions it is making need to be in the module. Ergo, you should only have to scan the module itself to figure out whether the code is unsafe or not, because if you can't prove safeness by looking at the module it's ipso facto not safe.