Are unsound type systems wrong?
frenchy64.github.io
frenchy64.github.io
Re: TypeScript:
> TypeScript challenges the status quo, claiming that lowering the cognitive overhead of using types is more important than type soundness. They argue that JavaScript programmers, their main audience, would find it easier to use TypeScript if they deviated from traditional norms.
Im not sure about the official mission statement, but as far as I understand, the purpose of their typesystem is to allow static description of the way existing JavaScript is typed, de facto, in the wild. This explains why e.g. literal strings are a type so you can do:
interface Eventor {
on('foo', FooHandler);
on('bar', BarHandler);
}
TypeScript was not created in a void, as a fresh, new typesystem. It was created to formalise the way existing JavaScript was informally typed. It would have been nice to see a little reference to or acknowledgement of this.
Or an example of how this could have been achieved better; preserving type soundness.
Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed.
So basically typescripts type system doesn't match the language semantics so type checked programs may crash at runtime.
The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.
Map map = new HashMap();
map.put("one", 1);
class Whatever {}
Map<Whatever, Integer> whateverToIntMap = (Map<Whatever, Integer>) map;
Integer i = whateverToIntMap.get("one");
System.out.println("i = " + i);
i = 1
You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that)
ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
The issue here is first order logic is complete for statements that are true for all models of the axioms. As an example, imagine a infinite land which cant be completely described by any computable map(a programmable set of facts about the territory). The map will only tell you some true things about the territory.
But we can say this - if there is some statement that the map cant decide, then there are two different territories for both of which the map is accurate, and the statement is true for one territory and false for another. So the deductive system is complete description of true statements which hold for all territories for which the map applies.
But if we are interested in a single given territory, no computable system of facts suffices. For example deciding whether a diophantine equation has solutions in the standard set of Natural Numbers or a more familiar example for this site, whether a program halts. No computable deductive system(ie there is a program which generates all deductions) will suffice.
Can you please recommend a MOOC/resource for learning more about this?
There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way.
https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
I like this definition. Can someone link to an authoritative article that elaborates on this statement?
> Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.
https://en.wikipedia.org/wiki/Soundness#Relation_to_complete...
You could probably follow the references there to more authoritative sources.
Programs that can be typed will not necessarily be typecheck-able successfully.
(I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
The type-checker 'proves' a statement of the form 'this program will never give values of one type to a statement expecting an incompatible type'.
The fact that a Java program can pass typechecking, and then throw a type error at run time, is proof that Java's type system is unsound.
https://dev.to/rosstate/java-is-unsound-the-industry-perspec...
In the other one, the first phrase uses "program that typechecks" and "is valid"; the second phrase uses "valid program" and "can be typed". "is valid" and "valid program" are equivalent, but "program that typechecks" and "can be typed" are not.
So the two completeness/soundness definitions taken as a whole are not equivalent. That's what I was trying to get at with my example - it's not that the exception throws, but that the exception even exists.
"Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at runtime. If the type system is sound, and the compile-time type checks all pass, then it is impossible to hit a runtime type error. More formally, a program is valid if the execution within the operational semantics (basically, the semantics of running the program) do not lead to an error. This is distinct from type checking correctly.
Similarly, in formal logic "true" and "provable" are not equivalent. We'd like them to be, for sure, but the various incompleteness theorems ensure that we'll never be able to prove every possible true statement.
This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.
> "program that typechecks" and "can be typed" are not [equivelent]
Sure. The above statement be more rigorous if it said 'has consistent types assigned to it by the type checker' and 'will be assigned consistent types when run through the type checker'.
[And, yes, every runtime ClassCastError demonstrates Java's type-checker's unsoundness, and a 'Sound Java' would have no need for the concept]
So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof.
Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)
That's in the line of Erlang's Dialyzer (one of the earliest "gradual typing" tools I know of), which also had to contend with actually being useful and being able to type actual usage patterns of existing years-old codebases..
Anecdotally, as an Elixir developer, I find Dialyzer to be pretty OK. Sometimes it misses things I think it should catch, but you quickly learn ways of structuring your code to help it more (not abusing macros, for one). We made a decision in the infancy of the code base to mandate typespecs for every function (both public and private) in the code base, and it has paid off in strides if for nothing else than documentation when you open a module you haven't touched in months. It catching bugs at CI time is a huge bonus. The error messages are... not great. I have it on hold right now, but I've got a branch for improving all the error messages in Elixir.
Many library authors are unfortunately not very diligent in speccing their programs. My first contribution to a dependency we use is often fixing their type specs to allow our code to type check. Some don't even bother putting in typespecs and Dialyzer gets upset because there's code paths it can't quite figure out, or even worse when one is wrong really deep in the middle. Seeing 80 errors in bright red because of a widely used utility function saying it returns a String.t() instead of an integer can be frustrating.
Re: CI, due to Dialyzer's persistent lookup table (PLTs) for all your app dependencies taking FOREVER to build from scratch, we had to do some trickery to get it cached as an artifact for future builds. But once that got working, CI got very snappy. It's really determined as a function of the triplet (erlang_version, elixir_version, the hashes of all your dependencies), so you can do things like create a docker image with a tag that is a function of that triplet.
For example, in lots of strongly typed languages when you make a sum type there's a constructor. haskell,
data Foo = Baz | Bar
or rust, enum Foo { Baz, Bar }
Baz and Bar are data constructors, they allow you to pattern match on them and make new values. In ts an equivalent sum type has to use a string/number refinement.
type Foo = { kind: "baz" } | { kind: "bar" }
This fits closer to js semantics and still allows sum types to be written. Unfortunately the pattern matching isn't anywhere near as good, but I applaud them for adding this to the language.
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 .
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.
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/theo...
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.
The op didn't say "safe rust", that's my point.
Btw, Java is unsound; see 'Java and Scala's Type Systems are Unsound - Semantic Scholar' ( https://pdfs.semanticscholar.org/3705/c660290e98877f882cf908... )
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.
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.
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.
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.
I do think the significance of Rust's unsafe keyword is exaggerated sometimes. It is just a bit of linting automatically provided by the compiler. Block scoping and tagging of unsafe code doesn't in itself add any guarantees. It's only barely more useful than a simple comment saying "beware: unsafe code here".
It's like having a Trusted Computing Base which is very small, verifying the hell out that TCB and then relying on its invariants when building up the rest of the system.
C++ cannot do this at present because all code must by definition be treated as untrusted/unsafe. In Rust you simply don't have access to do e.g. pointer arithmetic in safe code and that code is kept separate from unsafe code by the compiler.
(Modulo compiler bugs, etc.)
No, it isn't, because it may call code that uses unsafe constructs. (That's why you don't have to put an unsafe block around your code every time you push a value into a vector.)
>C++ cannot do this at present because all code must by definition be treated as untrusted/unsafe.
No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience.
For the last time: if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe, and safe code calling it is guaranteed to be free of data races and memory safe.
> No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience.
That wouldn't solve anything at all. C++'s type system cannot and does not enforce safe usage of APIs like string_view; it doesn't matter whether the safe code is using "unsafe constructs." If you choose to mark all C++ or C libraries that rely on invariants that can't be proven safe by the type system as unsafe, you will quickly find that essentially your entire program is covered in an unsafe block. The difference in Rust is not that it has unsafe blocks, but that its type system can safely encapsulate interesting APIs whose proof of safety is nontrivial.
Yes, I know, but lomnakkus said "code NOT bearing the [unsafe] tag is guaranteed to be memory safe" without adding this qualification. Without the qualification, the statement is incorrect.
>The difference in Rust is not that it has unsafe blocks
Indeed. That’s what I said above.
For some reason, Rust advocates don't like it when people point out that unsafe blocks, in and of themselves, do not add any kind of safety guarantees to the language or limit the effects of unsafe code.
Of course Rust's type system is able to express important invariants that C++'s type system can't, and this can be used to prevent iterator invalidation etc. etc. The point is that if you do have an unsafe block in your own code, you are going to have to go to the trouble of constructing a formal proof -- using tools that haven't been fully developed yet -- in order to be sure that any of the rest of your code is safe. And at present, the proof requires a translation step, which cannot be formally specified, from Rust code to LambdaRust code.
Rust is undoubtably much safer than C++ in practice. I just think the extent to which it provides hard and fast safety guarantees tends to be exaggerated somewhat in its marketing.
Not only that, but thanks to Rust's type system being able to express separation logic invariants, we may be able to do many functional proofs of correctness more easily; right now, refinement types are mostly limited to systems like Liquid Haskell because it is hard to generate invariants for impure code, but by integrating with Rust's type system such things become possible. There is at least one research group currently investigating this possibility, and it looks quite promising. Such work entirely depends on the fact that safe code that passes the borrow checker must be memory safe and has enough annotations that resource aliasing can be determined statically, freeing programmers from the burden of manually specifying primitives like separating conjunction and magic wand. Invariants would be stated at the function level and verified modularly (on a function by function basis), rather than current state of the art techniques used by model checkers, which usually require whole program verification. This has the chance to put scalable formal verification of functional correctness for many common errors (like integer overflow and out of bounds array accesses) in the hands of programmers who don't have training in formal verification; I find that very exciting!
I'd also add: requiring the keyword unsafe actually is fairly important in practice. Without it, there wouldn't be a way to assert to the compiler when a block of code that used unsafe primitives was safe (I suppose you could use something like "trusted" to mark a block safe instead of "unsafe" to mark it unsafe, but I suspect the ergonomics of that would be fairly untenable). So it's not entirely right to say that unsafe is pointless; it's a necessary component. It's just a trivial one.
The issue for me is a common misperception about unsafe blocks that the Rust community seems reluctant to squash. All I did in this (huge) thread was point out that unsafe code in an unsafe block can screw up 'safe' code outside the unsafe block. That is simply a fact about how Rust works.
The response in this case has been to go off on all kinds of tangents about formal verification that have little relevance to everyday Rust coding. Joe Coder's not going to formally verify his implementation of a doubly-linked list that uses a couple of unsafe pointer operations. It's probably best if he's aware that strictly speaking, none of the code that uses that implementation is guaranteed to be safe.
This is fundamentally the same kind of encapsulation that 'modern' C++ uses (unsafe code with hopefully safe wrappers), with -- as you point out -- the significant difference that C++ has a type system which would requires runtime checks to enforce certain guarantees that can be verified at compile time in Rust. (I believe it is possible to write C++ containers that catch invalid iterators at runtime: https://ac.els-cdn.com/S1571066111000764/1-s2.0-S15710661110...)
> Without [unsafe blocks], there wouldn't be a way to assert to the compiler when a block of code that used unsafe primitives was safe
Well, sure, but that's something that could be done by a linting tool without any significant loss of functionality, so far as I can see.
When you talk about formal guarantees, you are inherently talking about formal verification. I think it's pretty disingenuous to claim that such talk is irrelevant here; at least to me, it's highly relevant, and I really do care about being able to formally verify code on top of Rust. However, even if that doesn't happen, Rust is still in pretty good company re: safety; pretty much all industry languages expose a C FFI, which means that theoretically all their safety guarantees are completely out the window if even one C function is called (there are people who are working on formally verified safe linking, but the work is still very early). The C FFI is usually wrapped in something that is (hopefully) a safe wrapper, though not always. This is exacerbated by the fact that most languages' type systems can't actually enforce the sorts of invariants that C code needs (for example, a lot of older C libraries use static data in a non-thread-safe way; most languages can't design APIs that require calls to a library to stick to a single thread). Since most of the code in those languages is written in the safe subset, it's nonetheless pretty easy to find the (broad) culprit for a segfault when something goes wrong, and over time most safe languages develop their own safer alternatives to the unsafe C libraries (where possible). The hope (my hope, anyway) is that over time, more and more Rust can transition to the safe subset (which may require extending the type system), and much of the Rust that can't is formally verified. I don't realistically expect that all Rust will be so verified, but I do hope that (1) if you want to, you'll be able to formally verify realistic, large programs, and (2) even those that don't have few enough bugs that it becomes very difficult for attackers to exploit them.
As far as the link you posted goes: being able to catch iterator invalidation at runtime in the presence of multiple threads incurs a pretty nontrivial performance impact (Java, for example, doesn't consistently detect it in the multithreaded case). I wrote this before I even read the article. In the article, they explicitly did not consider multithreaded programs (which is true of most such articles). Despite that, while some operations were within 10% of the unsafe version, or even faster, others were anywhere from 2 to 7 times slower. Despite the article's claims, I don't see any reason to believe that the slow variants are less common than the fast ones.
And unfortunately, iterator invalidation is not some isolated issue: it's a common example of what Rust can guarantee, but it stems from the much more basic issue that updates to data structures with restrictions on legal byte patterns must be restricted in the presence of aliasing. Updating a C++ variant at all, for instance, is not safe without strong aliasing guarantees, even in the single threaded case. For a substantial amount of C++ code, you'd have to either go the Java route (make every data structure valid after any word-size partial update, so all operations can be weakly atomic, at the cost of losing interesting mutable in-place data structures and not being able to perform some common compiler optimizations), or wrap updates to many kinds of values in mutexes (which would completely destroy performance in most cases). "Just do it at runtime" has severe performance tradeoffs in the domain that C++ is targeting; requiring shared_ptr to be atomic in the presence of threads is already bad enough that many larger projects write their own custom reference counted types (whose correct use can't be verified at compile time). If people were willing to eat it everywhere, I think they would have switched to Objective C or Swift by now, which use clever tricks to reduce the impact of pervasive reference counting. To see some examples of how this would have to work, see how Swift handles things like string slicing (and compare it to the Rust or C++ versions).
The reason I can say all this pretty confidently is because Rust has dynamic safety mechanisms as well. In almost all cases, you can choose between four options: a relatively cheap (but expensive space-wise) single-threaded version, an almost free (but restricted in functionality) single-threaded version, an expensive time-and-space-wise (and relatively general, but still restricted) multi-threaded version, and an extremely restricted multi-threaded version that can't handle interesting updates. People usually opt for a single-threaded version where they use it at all, because they cannot eat the performance and functionality impact of the multithreaded one. If you try to enforce safety with dynamic checks in C++, you will lose to Rust on performance; in fact, you will probably lose to Swift (which is designed from the getgo with these tradeoffs in mind).
In short: even single threaded dynamic validation can have a noticeable performance impact. The bare minimum you need to be competitive with Rust and remain safe is distinct single-threaded and multithreaded dynamic mechanisms, together with the ability to reject code that misuses them at compile time; these mechanisms can only handle aliasing tracking and do not replace the functionality of lifetimes, which can only be relaxed using unique ownership, reference counting, or leaking data. Static thread safety verification would thus need to be restricted to data without references. Given all this, I believe that the only way to make everything work dynamically would be to disallow first-class references entirely in C++. That would break almost all C++ code in the wild, and would make its runtime model comparable to that of Swift. Common tricks to get around reference counting in Rust (like arenas) would necessarily have a large performance impact in this model, and would probably not be used much. Modern or not, C++ doesn't encourage writing code in this way.
> Well, sure, but that's something that could be done by a linting tool without any significant loss of functionality, so far as I can see.
It can't be done by a linting tool, because a linting tool has no idea whether a particular use of unsafe code is well-encapsulated or not. The only way we know how to prove this right now is using formal verification, so we assert safety of such code with manual annotations. I really should have mentioned the alternative as "declare everything that isn't allowed to use unsafe code as `untrusted`" because that's the actual alternative; marking well-encapsulated unsafe code as trusted is actually how things work today. I hope you can see why having the default be "trusted" is not a satisfactory alternative for a language that wants the default to make writing safe code easier than writing unsafe code; you should have to opt into being able to shoot yourself in the foot, and it should be easy to find code that claims to be upholding invariants.
Not so sure about that. I wrote a parse tree transformer in Rust and wanted to write a mutable iterator for my parse tree. That requires unsafe code. So you don't have to be doing anything particularly esoteric to require a small amount of unsafe code. Writing a small amount of unsafe code is not the end of the world, of course. I am not saying that this is a major flaw in the language.
Re catching iterator invalidation at runtime, I should have said explicitly that I was not claiming that this is as good as catching it at compile time.
>It can't be done by a linting tool, because...
I meant that the functionality provided by the 'unsafe' keyword itself could be enforced by a linting tool. (E.g. any block that uses one of the unsafe operations must contain a comment saying 'unsafe code here'.) If this isn't the case, I must have some fundamental misunderstanding about what the unsafe keyword does. The Rust docs suggest that it simply enables a small number of unsafe operations such as pointer arithmetic.
Of course the idea is that you limit the unsafe stuff to small areas of the code so you can really think through those parts to make sure they do what you think they should do. Another thing that's nice about containing the unsafe code to small blocks is that you start each unsafe block from a state of the program with all the guarantees from the surrounding safe code, which makes it easier to recognize what could go wrong in the unsafe code.
But in general you're incentivized not to lie (and not to trust liars), so while its not provably "safe" to use, we can show everything else is safe as long as the assumption holds.
The type system is sound, where it exists (in "safe" rust), and not sound where it doesn't (in "unsafe" rust).
In the same fashion that nothing is sound if you don't trust your cpu to perform primitive operations correctly. But if you do trust it, then the type system has a chance at being "sound".
Right, but the same can be said for C++. If you can trust all of your not-provably-safe C++ code to be safe, then you can trust your whole codebase to be safe.
Object ownership specifically is the biggest problem, you can enforce usage of shared/unique ptr everywhere but there are still instances where you might have passed a reference or raw pointer somewhere and then the last owning pointer goes out of scope in a callback function and the reference will point into whatever. Static allocation can solve a lot of this but then you are very constricted to the types of programs you can write. These are all the problems that the borrow checker avoids.
I've used many static analysis tools and seen many things they can't catch, one example is if you forgot to check if your std::map::find returned end() before using the result? If you do so you are suddenly reading or writing into random memory.
And by limiting the attack surface the language becomes safer. Not formally, but in practice.
You have to go out of your way not to stay in safe for the most part (if rust's design does what they intended), which implies that most of your code should be provably safe (by rust's definition of safe), as long as the ideally small unsafe blocks are correct, if the program compiles.
Where in C++, there is no such gaurantee regarding compilation; even your "safe" code isn't shown to be safe by the compiler (additional tooling may apply further checks); your whole codebase is assumed to be unsafe.
The "potential problem" is naturally the size of your codebase, whereas rust offers it as a subset of the codebase.
You can focus your manual verification efforts on unsafe code. That is pragmatic. “Well, shit happens, and I can do nothing about it” is not.
>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.
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....
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.
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
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.
The important thing that is different about code proved in Rustbelt is that the guarantees can be made local. Once you prove a semantic type for a particular piece of unsafe code, you do not have to know anything about that unsafe code when you prove some other piece of unsafe code correct, as long as they are independent of each other (including unsafe code that is invoked parametrically). This means that the proof effort does not scale with the size of your overall code, or quadratically with the number of unsafe modules, but linearly with the number of unsafe modules. That's absolutely not true in C++; it works entirely because of Rust's precise accounting of ownership.
Finally: even in Rust that uses a lot (relatively speaking) of unsafe code, only a small percentage of the overall code is unsafe. Typical codebases have many hundreds of lines of safe code per line of unsafe code. This means the proof effort is quite reasonable. Automated proofs about C and C++ programs are not trivial and all known techniques do not scale to real code that is more than a few hundred lines, and proof assistant based techniques generally must either prove things about the entire program, or use restricted subsets and annotate them with information very much like what is in Rust's type system. The sel4 microkernel is one of the largest formally verified C programs, and it took 20 man-years of effort and hundreds of thousands of lines to prove, while the actual C code clocks in at under 10,000 lines. While the sel4 proof effort cared about more than memory safety, a significant amount of it was devoted to that. By contrast, I have personally written 10,000+ line Rust codebases with 4 lines of unsafe in them (and even those could be avoided if I were willing to sacrifice a bit of performance); I used only a few standard library functions, and third party crates like Rayon that have undergone a fair amount of verification effort themselves. Memory safety in Rust actually scales to realistic codebase sizes.
The existing result isn't everything; there is still a lot of work to do to make sure it's accurately capturing all of Rust's semantics. But most of the "hard parts" have been done--we are pretty confident that the encapsulation I'm describing actually works. That is far better than the situation in C++.
Not that this takes away from your larger point exactly, but Java+null is no longer a good example.
* 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
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?'.
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?
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.
Here's some code which is syntactically legal in both TypeScript and Flow, but the languages disagree on whether a type error is present:
type T = { // Legal decl in Flow, illegal in TS
x: number;
[s: string]: boolean;
};
const m: T = { x: 1, xz: true };
m['xz'.substr(0, 1)] = true;
m.x.toFixed(); // Crashes
Yet in JavaScript this is an extremely common pattern - an object bag where some known property keys have a certain type, but "all the others" have a different type. You can't represent this in a bolt-on type system without forcing the developer to jump through enormous hoops proving that any lookup key isn't one of the "known" keys. By enforcing soundness at all costs, you lose the expressiveness needed to ergonomically describe this object.
Since most people don't directly aim guns at their feet, the unsoundness here is unimportant in practice. This is one place where I think Flow made the right trade-off to be unsound for the sake of practical usability for a common pattern.
Coming from Haskell, the level of unsoundness in Flow is very grating, and I would honestly not recommend it over untyped JavaScript... It luls you into a false sense of confidence that the program is correct, without it actually being so.
TypeScript is a lot better in that area.
This line must only be accepted if a proof that 'xz'.substr(0, 1) != "x" is provided (for instance, inferred from a runtime check or encoded as a type) [obviously, that's impossible with that specific value]
While "unergonomic", code that doesn't do that is just broken and might for instance result in a security catastrophe if the key is attacker controlled.
If you have a sound type system, it's harder to write code but the compiler and IDE can infer useful invariants and give you guidance in return.
If you have no type system, you're on your own with error detection, but writing code may be a lot faster.
(Though I personally think a modern language with sound types and useful type inference can solve a lot of the tedium as well)
If you have an unsound type system you get the worst of both worlds: You have the cognitive overhead of a typed language but at the same time don't get any of the guarantees and invariants.
Yes, there are cases where you will not find an error until run time. Debugging this is identical to debugging that same error in Javascript, because you know you don't have guarantees from Typescript.
The more strict your type-system is the more things you can prove and thus understand about your program. But if you need to change your program it may no longer compile with the existing types. Does your type-system then make it easy to change your types so they reflect your new program?
Now assumably when you are developing a new program it is changing all the time. If you fix its types early doesn't it actually make it more work to create your program?
Once your application is done and works and is big it is essential that it is "typed" so that you can see what changes don't require changes in the types vs. what changes would require a lot of rewriting of the types all over the place.
I think the fact that many useful programs are written in dynamically typed languages speaks for this. Small programs don't need types.
Does this mean that optional typing is a good feature?
Furthermore, usually development uses type system as a tool, so it'd be hard to add typing when it's done. (I mean, usually functional doneness is checked or "asserted" in a large part through types, and unit/integration tests help with the rest.) So in this sense typing doesn't add more development time. It just makes problems a lot more explicit, so you know you're not done yet.
Your declared types are the shared "language" under your program. It is much harder to change the language that what is said in it. Changing the language would actually change the MEANING of what has already been said.
Yes. The type system in fact makes it easier to make this kind of change, because when I change one of my assumptions (e.g. I say "the input list to this function must always be non-empty") the compiler tells me exactly where I need to make a corresponding change.
> Now assumably when you are developing a new program it is changing all the time. If you fix its types early doesn't it actually make it more work to create your program?
Fixing the types early would indeed be a disaster, but why would you ever do that? Types are something that evolve and change as the program does, just like e.g. variable names.
It's basically like using and debugging C/C++ code, where it looks like there is a "type system" but in fact you are just arbitrarily manipulating a big byte array that contains all your data and the call stack (except with TypeScript it's a graph of untyped arrays and dictionaries instead).
In fact I do not know of any language that is actually safe at it's FFI boundaries. Rust isn't, Haskell isn't. You could get a value back from a C function that you were told would be allocated 64-bytes and actually it was only 32, so you'll have an overflow somewhere later. The Typescript / Javascript boundary is similar, though obviously not as dangerous.
I still like your analogy, as when things are down executing it is as you say just on big byte array, you should never try to map this array to the language manually though.
A simple example of python2 that would make developers brought up on a healthy diet of haskell cringe is this:
>>> for x in range(100): print type(1<<x)
type(1 << x) is int for small x, but long for large x.
https://docs.python.org/2/library/stdtypes.html#numeric-type...
"Plain integers (also just called integers) are implemented using long in C, which gives them at least 32 bits of precision (sys.maxint is always set to the maximum plain integer value for the current platform, the minimum value is -sys.maxint - 1). Long integers have unlimited precision."
The distinction between plain and long integers is gone in Python 3.
- "Number", which would be the generic DWIM arithmetic type. In your example both x and the literals would be Number.
- Hyper-specified arithmetic types. Not just number of bits and signedness, but also overflow and trap behaviour. Less convenient to use - you can't easily add a "32bit signed wrap on overflow" to "16 bit unsigned saturate on overflow", but have the advantage that there is no unspecified behaviour. This also allows the user to make use of machine-provided saturate and overflow behaviour where present.
My idea is to let programmers specify various constraints they care about on numeric-typed variables, including min/max value.
Then the compiler has the freedom to choose any representation(s) it cares to that matches the constraints.
For complicated constraints that are difficult to prove at static-compilation time, some checks might be deferred until linktime (when static call contexts are available) or runtime.
C offers a fairly small choice of types to the programmer, certainly compared to one of the ML/Haskell style of language. It doesn't even have a proper "string" type!
C doesn't exactly allow mixed-type expressions, it just performs a lot of type coercion and reinterpretation. Which is another one of those things that trades safety for convenience in so many languages.
Type flexibility is responsible for most of the wtf type moments in Javascript: https://www.destroyallsoftware.com/talks/wat
The type systems we're talking about in the OP article are about proofs that can be made over the code before it is ever executed. Dynamic type systems make few claims here so they don't cause issues. What does cause issues is asserting something to be proven true, but having compositions in the language that make the assertion false.
dynamic -> dynamic -> dynamic
<< :: Integer -> Integer -> Integer
edit: saw union/intersection types mentioned in another comment - I guess that's what you were referring to?
Sum types are essentially discriminated unions. Given a value of a sum type, it is possible to tell which alternative it is. This is commonly done through pattern matching.
Union types are a bit like C's undiscriminated unions in that you cannot tell what the actual type is. This makes them significantly less useful, and thus very few functional languages have them. Essentially when you get back a union type of A | B, you can only perform actions that make sense on both of them. This essentially means functions with a type variable (parametrically polymorphic) in typical functional languages. If we additionally have subtyping (which ML-like languages don't) this can be more useful.
Side note: things like the `typeof` operator in JavaScript is muddling the water a bit. But I'm talking about the theoretical perspective.
<< :: Int -> Int | Long -> Int | Long
<< :: Long -> Int | Long -> Long
>>> -1j * -1j == -1
>>> f(-1j * -1j) == f(-1)
I think there are many such ways we are held back by plain text representation.
Haskells approach to this keeps the constraint of soundness: https://youtu.be/re96UgMk6GQ?t=52m5s
The whole video is very interesting even if you know nothing about Haskell, but are just interested in language design in general.
To summarize the part of the video I just linked: Their approach so far has been to try and design the type system in such a way that you reduce programmer pain while not sacrificing soundness at all. It is a painful constraint for language designers, but it allows you to gradually add functionality to the type system from observing real world examples. The goal can be described as: Design a typesystem such that every working program can be typed in both a sound and correct way, while minimizing the amount of programs that can be typed, but are not working as intended.
In Languages like Haskell or completely dependently typed languages it would be morally wrong (in my opinion) to have an unsound type-system. Here the role of the types is different, you use types to compute types and need to trust the compiler in complicated situations that this is sound, just like you trust the compiler to do correct floating arithmetic. Checking the types per hand may be a real challenge, for example if your writing super polymorphic code. Sometimes you even have to prove that your code fits the type-signature (per induction etc.), here you want guarantees.
Not sure what the article is referring to here...
Java soundness issues like array covariance, final field mutability, unchecked generics casts, etc were definitely surprises to many users, but the Java language designers were well aware. They added runtime checking to make sure those soundness holes didn't cause the JVM to crash or violate the security guarantees.
Sure, there were some additional surprises, but I'm sure TypeScript has had many more. (Partly because the TypeScript type system is more complicated, but also because it's not important to get it 100% right -- JavaScript runtimes don't perform optimizations that rely on the soundness of TypeScript.)
Now, there are distinct disadvantages to unsound type systems, but that doesn't make them "wrong". I love Python and sometimes wish I could turn on a switch in the interpreter that made it statically typed, but there is no denying there is a freedom and (initial) productivity boost in ducktyping.
Other than that it really depends where. How bad unsoundness is depends on how sneaky the resulting errors are and how hard they are to debug.
[1] https://github.com/mobxjs/mobx-state-tree#thanks see tcomb
Types as „approximation of the result of a computation„ is also a nice and concise way to describe them, haven’t seen that definition before.
Soundness only provides a guarantee if you control when and how your code will be executed, and that's a tough constraint. To prove is not to forsee the future.
Which properties are you referring to? My understanding is that ES6 is back compatible and so that can't be case. There's "use strict" but that's a different kettle of fish; a pragma that changes runtime behaviour..
The most common JavaScript error I encounter is accessing fields of undefined objects.
Can't we simply have a type-system for JavaScript that only prohibits undefined field access and nothing else?
If we accept that the system will be unsound anyway, why not focus on the main benefit and throw all the baggage out?
Yes, but it's not easy for cultural reasons. In order to detect undefined field access you need to know what the fields are at compile time, which is to say, you need classes. Javascript's original design was based on prototypes, which have a fundamental "impedance mismatch" with classes. It's possible to layer classes on top of prototypes. That's actually not so hard, you can find a lot of user-level implementations of classes out there (e.g. https://github.com/neverblued/js-clos). But to make that part of the language so that compilers will be aware of it you'd have to get the community to agree on a design, and that is very challenging. But it's a political problem, not a technical one.
TypeScript has optional null checking if you want it. Given that it supports union types, null/undefined tracking fit nicely into the language.
https://blog.mariusschulz.com/2017/02/24/typescript-2-2-the-...
(Downcasting from * in a gradual type system is analogous to how C lets you cast from void* to any pointer type implicitly, except that RTTI checks that the cast is safe.)
Neither unit testing nor contracts are verification tools.
After switching all my JavaScript Dev to ts a couple years ago, I cant imagine how I would get by without it.
- type inference
- structural types
- union and intersection types
- important: easy escape hatches such as trivial cast to `any` or the ability to write your own type definitions for almost any random piece of code including third party libs
Type purists may scoff at Typescript's type system, but it's there, it mostly works, it's very easy to get started with, it's reasonably fast. I would personally wish for exhaustive type checking, and I wouldn't be surprised if I get my wish sometime in the future.
Another rather pragmatically typed language is OCaml/ReasonML
It is possible to encode the semantics of exceptions such that a reasonable definition of soundness is still provable. See, for instance, Chapter 14 of Types and Programming Languages by Pierce.
That's not interesting. TypeScript did things in way Y, different from the usual way X, and some academics realize they get a free paper out of reimagining TypeScript doing X.
Let us synchronize ALL of the computers, while we’re at it.
Also, suddenly cryptography and computers are cool :)