It would be nice to have some examples of what these terms mean, for type system dilletantes like me. I must say, I was a little lost :)
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:
Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it). And, I assume, covariant arrays.
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.
While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress).
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.
Note that most common type systems "crash" type-checked programs at runtime: null-pointer check failures, array-bound check failures, and (even, Java) co-variant array write check failures. So the line is fairly fuzzy.
Or just silently fail! Knowing the history of the Collections API and generics in Java, I know WHY this is like this, but Map.get taking an Object has resulted in way more bugs in previous code bases than I'd like to think about. If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map. You can of course wrap that call behind functions that DO check the proper input type, but until you've been burnt by it you might not think to do that.
> If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map
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);
Prints:
i = 1
That's a consequence of generics type-erasure for backwards compatibility with non-generic code, so there _is_ a reason for `get` accepting any Object.
Like I said, I know the history and why it exists. I learned Java before 1.5 came out. That API existed long before generics did (I think 1.0 or earlier). If they had designed the language with generics in mind, they would have probably done it differently; hindsight is 20/20. Doesn't make it not a suboptimal API. I don't think there's a good way to fix it this late in the game without breaking old code, but such are the warts of backwards compatibility.
Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).
Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
(It's been a year and a half since I took a course on this, so I apologize for any mistakes)
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.
We can state a lot of things in first order logic about natural numbers or set theory which are not provable (in some given set of axioms like Peano axioms or ZFC, you can extend the axiom set but then one can generate a new unprovable statement if not a contradiction).
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.
My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook.
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.
Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?
This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia:
> Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.
Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular.
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.)
In the Wikipedia definition, the first phrase uses "all provable sentences" and "are true"; the second phrase uses "all true sentences" and "are provable". "true" and "provable" are equivalent in the two phrase here.
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.
> Similarly, in formal logic "true" and "provable" are not equivalent.
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.
The distinction you're drawing is imprecision in the type-checking statement.
> "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]
I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right?
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 :-)
> Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it).
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.
I kind of found Dialyzer disappointing from starting a project from scratch. It would miss many obvious mistakes that I expected would be caught. Very much was not a fan of this key design decision of success typing! That said, the theoretical research behind it I can respect.
I think another reason they added refinement types in the form of literal string types and literal number types was because there are no data constructors in TS & Flow either. This is a bit of speculation on my part.
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.
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'".)
> 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.
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.
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.
Is this the same thing as the terms open-world vs closed-world soundness the article uses? I.e the API is sound but it uses unsafe on the inside? I've never heard those terms before.
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?
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.
> 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.
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.
> 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.
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.
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.
Ok, but then that is true in any language that allows unsafe code. You can also put raw pointer manipulation in a module in C++ code.
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".
The point isn't to tag the unsafe code. The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions.
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.
>The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions.
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.
> 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.)
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.
> if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe
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.
Sure. There is a lot of work left to do to bridge the gap between the formal model and Rust code. But we can be reasonably confident at this point that the libraries we've proven correct actually are correct (modulo translation errors), and we specifically set out to prove things about libraries that were safe for interesting or nontrivial reasons. That's a huge step forward. It means that, with some time and effort, producing codebases with formal proofs of memory safety can be done at quite low verification cost. The executable might need to be generated with something other than LLVM, of course, but using tools like CompCert is possible in these cases; the primary difficulty with it is normally that it only correctly compiles correct C, which is difficult to find in the wild to say the least.
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.
I don't deny that Rust's lifetimes make it possible to provide static guarantees that C++ can't.
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.
Frankly: Joe Coder isn't implementing a linked list in Rust. I encourage you to take a look at most of the repositories we can find on Github; while many use unsafe (mostly to call out to third party C libraries), very few are doing so to create nontrivial data structures. Obviously, each usage of unsafe has the potential to destroy all memory safety guarantees for the program, and I personally think people reach for it much too frequently. Nonetheless, if something goes wrong, people know where to look; as it turns out, it is actually possible that the unsafe code is correct even when it lacks a formal proof (only two memory safety errors were found during the verification effort, that I'm aware of). One hopes that the likelihood of this code being correct goes up significantly when there is less of it and it is marked for extra scrutiny (I certainly know that my first reaction when I look at a new Rust repository is to search for `unsafe` and see what bugs I can find).
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.
>Frankly: Joe Coder isn't implementing a linked list in Rust
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.
Well, it's pretty trivial, but there are a few subtleties. Keep in mind that unsafe has another meaning when attached to a function type or trait, which interacts with the type system. That can have surprising but necessary consequences (such as not being able to pass an unsafe function as an argument where a closure with the same signature is expected). But yeah, it's not really a first class type and it has deliberately simple semantics, so if you just want to replicate the exact functionality of unsafe in Rust you could probably do it as a lint (though for stylistic and ideological reasons I don't think Rust would ever consider doing so).
Yes, that is correct. In theory, a single incorrect unsafe block can have effects on every other part of the program.
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.
I think the idea is that you tell the compiler to assume that this particular chunk of code does no wrong, and compiler shouldn't bother to try to prove it. Of course if you lie, then everything else can break down.
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".
>I think the idea is that you tell the compiler to assume that this particular chunk of code does no wrong, and compiler shouldn't bother to try to prove it. Of course if you lie, then everything else can break down.
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.
Ya, the difference is that in your 1MLOC code base you only have to review 10k lines with a microscope instead of every single one, the rest you can more or less trust to not do any funny business (with regards to memory).
Not true at all. All the 'unsafe' keyword does is allow a bunch of code constructs which are not allowed outside unsafe blocks. You can just as well limit your attention to that subset of constructs in your C++ code. You can't do it by grepping for 'unsafe', but you could do it using a C++ parser.
Such a subset would be extremely limited and hardly be called c++ and i still don't think it would be possible, the problem is that these problems occur across files, not just because someone happened to use GOTO in isolation on line 123 in filexyz.cpp.
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.
Sure, but that has nothing to do with C++'s absence of an 'unsafe' keyword, or the presence of one in Rust. It has to do with differences in the actual language semantics (and in the unsafe design of the STL and common C++ coding practices).
It has everything to do with unsafe. Because outside unsafe you are forced to use the borrow checker, among other things, preventing you from thrashing memory with 100% guarantee. The number of ways you can thrash memory in c++ can't even by listed, especially not when it comes to object lifetime, so there is no equivalent subset of c++ providing those 100% guarantees. If you do such a mistake just once, the whole execution of the rest of your program might be randomized. Multiply all those possible mistakes with the size of your code base and you see the problem. In Rust, you have all these problems inside unsafe but the amount of code inside unsafe is much much smaller so it is feasible to only let your most senior guys write them and to review them extra thoroughly.
No, it has nothing to do with the presence of the unsafe blocks. Rust would be exactly as safe or unsafe as it currently is if the requirement to wrap unsafe operations in unsafe blocks were removed. The only difference would be that it would be more difficult to grep for code that used those operations.
Yes, one bad unsafe block in rust can screw up even safe code, everybody here understands that. The difference is that the potential problem surface is much smaller and it is obvious where it might be.
And by limiting the attack surface the language becomes safer. Not formally, but in practice.
How small the potential problem is depends purely on how much unsafe code you write, regardless of whether it has a special keyword associated with it.
You can imagine though, that the intended model for rust programming is to avoid "unsafe" as much as necessary. Essentially that C++ is using unsafe by default, while rust has safe by default.
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.
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.
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.
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."
> 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.
The situation isn't remotely similar to C++. After you prove an algorithm correct in C++, you can still generally not guarantee that it is used correctly by the program--the needed preconditions and postconditions are not expressible in its type system, and code that passes the C++ type checker can easily violate invariants elsewhere. In Rust, after you prove code in an unsafe module correct with respect to its type, you can use the module from any safe block and still preserve memory safety and data race freedom.
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++.
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.
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?'.
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?
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.
Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing that its purpose is not to eliminate any kind of error. This is why “mathematically civilized” is a much better term. For example, even if you don't mind null pointer exceptions, it is not mathematically civilized to add one extra case to everyone's case analyses.
Unsoundness is important because soundness and expressiveness come at a trade-off.
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
TypeScript is actually more sound than Flow in this example because it disallows the declaration of T in the first place. Flow allows this code and it fails due to a type error at runtime.
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.
Flow and its unsoundness is horrible. Quite often I can get runtime errors for code that compiled without warnings, and nothing for code that is showing warnings, because, amongst others, Flow's union type resolution is pretty abysmal.
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.
The problem lies in accepting "m['xz'.substr(0, 1)] = true;".
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.
"Will it be easy for a computer to prove that my API is being called correctly?" is not a question that JavaScript library authors seem to give any thought whatsoever to
That's generally not an option if the type in question is part of the interface of an external library. The type systems of Flow and TypeScript are both designed to allow typing of as much existing idiomatic Javascript code as possible.
To be honest, after reading this article, I don't really have more information why you'd want to use an unsound type system at all.
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.
From my experience in using Typescript, it is extremely useful. It catches most errors instantly in your editor so you can correct them before even attempting to run your program or tests. This makes coding faster for me, even though I also have to specify types. This is not "overhead" - working through type relationships also improves your understanding of the code you are writing - often you will find errors in your reasoning before you've even written the code, just because spelling out the types leads you down the correct path.
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.
A big advantage of unsound types is versioning. IE you can add some member variables/methods to a structure/class and users of that library that were written with the old version still work without trouble, recompilation or redeploying. Of course if you remove the variable they're in trouble but removing can be avoided for that reason.
In this sense typing is like unit-testing it would seem. You can make your program "better" by adding more unit-tests to it. But more tests you have the more work it will be to modify your tests, to accommodate the changes in your program.
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?
I usually find a lot more serious bugs in quick and dirty scripts, than in big systems, regardless of language. (Naturally, big systems have already survived the small PoC phase, plus usually big things are viewed as complex, whereas small scripts are dangerously innocent looking.) So in that way things like Ammonite (easy scripting using Scala) seem very useful - even if the runtime requirements are a lot heavier, than using bash (or python).
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.
Explicitly declared types are like anchors. They make it harder to change the program to be a different program. In many cases this is good since it tells whether a change breaks things or not. But it does add to the "mass" of your program, makes it harder to change its direction.
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.
> Does your type-system then make it easy to change your types so they reflect your new program?
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.
Yes: your program fails at runtime, and you have no idea of where the problem is, because the place where the type invariants are violated is not related to where an exception is thrown or an incorrect result is produced.
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).
It is absolutely no different from debugging Javascript. In Javascript you have an expectation of types in your mind, that are not guaranteed. The same is true of Typescript. The difference is, Typescript will catch most exceptions to the type system at compile time. It is not sound, but is extremely useful.
"Most" isn't necessarily a good thing, because it can lead to a false sense of security. For example, if you start thinking, "no need to check for null here, because the types won't allow it", you're open to being surprised when a null sneaks in at run-time. So you have to deal with the overhead of both types and run-time guards.
This is the sort of thought people have when they haven't actually used the language much. It is also an example of something Typescript is really good at. If you try to use an `any` value - or any nullable typed value - that hasn't been checked for null, it is a type error. Sure you could write a type definition for a Javascript function that is a lie and say that it cannot return a null when it can, and then guess what? You'll get a runtime error and debugging it is identical to Javascript.
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.
The problem is in just how much boundary there tends to be, since many TypeScript programs are heavily mixed with ordinary JS. I would agree with you for programs that exclusively use TS for application code.
It's not like it fails on a 1d20 roll. Most unsound languages will only cause runtime problems if you are proactively trying to construct things which defeat the type system.
People assuming C is a big byte array is one of the most common source of difficult to debug bugs. People write code assuming they can manipulate bits and bytes here and there using pointer arithmetic because "they know" that this offset into an array will align with this member of that type. Then they come crying that the compiler is broken and change their optimizer setting to -O0 ....
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.
It's an interesting question. It seems that developers are quite able to cope with weird type systems, moreover most of them don't even think about it or even care.
A simple example of python2 that would make developers brought up on a healthy diet of haskell cringe is this:
"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.
This kind of thing is why I'd favour two different types of numeric types:
- "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.
I see where you are coming from, but C offers a cautionary tale: It offers more choices than most languages, and that creates a number of traps for the unwary. Maybe, however, that is only because it allows mixed-type expressions?
Choice for the programmer, or choice for the implementer? Part of the problem of C is the amount of stuff with was left as a choice for the implementers on a particular platform and therefore could not be safely assumed to be universal. Forcing the programmer to enumerate what they actually want from their "fast machine integers" avoids that.
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.
That example isn't a type problem. With a numeric tower and polymorphic arithmetic operators, it's to be expected in a dynamic type system.
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.
That's because that's how dynamic type systems work, from a static typing perspective. They defer typing until runtime. Properties of the code proven before execution aren't usually very interesting.
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.
Yes, and it means (<<) is not closed over Int, which means that you will need to be able to compare instances of Int to instances of Long. Before you know it you're wondering what the result is of
>>> -1j * -1j == -1
and
>>> f(-1j * -1j) == f(-1)
where f is some pure function. Some people think it's the road to perdition.
Are you basically saying that programmers want intuitive interpretation of numeric literals, without having to suffix them to indicate their type? This strikes me as a situation where editing programs as plain text holds is back. Most languages have complex and error prone implicit type conversions between numeric types so to keep the text representation of the program looking clean. But if there were a way for the source to contain explicit type annotations on numbers without necessarily requiring the programmer to have to look at them or specify them in most cases, that seems like a much better situation.
I think there are many such ways we are held back by plain text representation.
Unsound typesystems are not necessarily a problem, but consider the problem the other way around: given a sound typesystem, how do we improve this in such a way that
a) the average Joe will understand it
b) it decreases the overhead of writing the types
c) the type system helps the programmer write better programs
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.
I don't really think that unsound type systems are wrong, because I think it depends on the role of the types in the programming languages. Typescript, Java etc. don't have that sophisticated type systems and you can just check the types for yourself very quickly. You rely on the type-system to correct obvious mistakes, but not more.
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.
> The way TypeScript was designed is in fact more promising than older systems like Java. Those systems inadvertently broke type soundness instead of making it a deliberate action.
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.)
Wrong? That's a bit of an odd question. It's only wrong if the context is, "what is an example of a sound type system?"
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.
Python does have static typing nowadays :) Checkout Mypy, and also Dropbox's PyAnnotate, which helps statically type existing sources by recording types during runtime and then adding them to the code.
I think some of the recent developments in run-time type checking systems like the one in Mobx-state-tree [1] and Clojures Spec [2] are interesting. I don't know enough about either to make any witty remarks but I'd like to see the impact they have on the field.
Most readable introduction to the topic I‘ve read so far. Nicely outlines the dichotomy between unit testing and types as both serving as different kinds of verification tools.
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.
TypeScript cannot be sound because its model of the runtime environment necessarily diverges from the runtime truth. A simple example: some properties were removed in ES6, so type checking against an ES5 runtime will result in type errors when run in an ES6 browser, and vice versa.
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..
> Can't we simply have a type-system for JavaScript that only prohibits undefined field access and nothing else?
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.
I think any in TypeScript's context means "not in the type system", and all type rules bounce off it. So if k's type is any, and you type k.foo, it doesn't bother checking it. I assume the same applies to any null checking.
The object type is the type of all non-primitive types, what you want is the Object type instead. Yes, it's confusing, especially as there's also the {} type! This article goes over the differences:
I feel like a distinction needs to be made between soundness and precision. A sound type system never tells you something wrong while a precise type system tells you everything that needs to be said about a value. Gradual type systems are imprecise, because they could type something at some * type. There's nothing wrong with that. Unsoundness is bad on the other hand, it keeps you from omitting dynamic type checks in places where you would want to in your compiler. A natural thing to want to do is include dynamic checks expressly where you are downcasting from a * type, omitting them where the type is known precisely enough. That is how you reap a performance gain from your type system, and unsoundness prevents you doing that.
(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.)
I tend to call Typescript's type system "pragmatic typing":
- 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
That's an unusual use for "type soundness". To me, type soundness has more to do with whether all the functions in a program are total, i.e. defined across their entire range of inputs (can't throw exceptions, can't crash, always return values belong to the return type they declare).
The author's use of "type soundness" matches the precise, widely-accepted mathematical definition which is used in the literature. Type soundness does not require total functions, although they certainly make it simpler.
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.
What is a high level type system anyway ? Annotations to help feed the intellisense engine, to warn about miss-spelled variables, make sure you don't use an apple where there should be a banana, Or are types just objects with limited states !?
> Interestingly, fixing these areas in TypeScript has been a fruitful source of new research
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.
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:
Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it). And, I assume, covariant arrays.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.