That being said, this is why I want to start to write more blog posts about Carp. I had to wade through the deep waters alone, with occasional help in the Gitter channel. Now I want to share that experience. As such, the blog post goes in a different direction than, say, Matsakis’.

In a perfect world someone who cares about communication and is good at it will be in the core team of the language at one point. In the meantime, we’ll have to make-do with me.

If anything, Carp's is an advantageous position relative to Rust: You don't risk breaking many other people's code by fixing any type safety holes you find along the way. Which you will, not because you're stupid, but rather because type system design is applied formal logic, and formal logic is frigging hard for humans.

> While I do agree with the fact that one of the best features of Rust is the communication

It's not just that they communicate something, but rather what they communicate. Most language designers that have a user community do a reasonable job of explaining how new language features solve existing problems users face. However, they usually do a poor job of explaining how new language features interact with previously existing ones in all possible cases, and the main reason for this is that language designers have trouble anticipating these interactions to begin with. In other words, language designers don't understand their own designs! Matsakis' blog shows that the Rust's developers do a much better job than other language designers in this regard.

I think we are on the same side of the fence. Reasoning about your designs—and communicating your reasoning openly, not fearing scrutiny but rather embracing it—are important in any project.

But you compare an introductory article in which I try to explain a language to prospective users or other interested parties with the notes, musings, and writings of someone working on a compiler, aimed at an entirely different set of interested parties. Sure, in the end we’re all programmers and should all be interested in both, but trying to cover both at the same time will only result in mental overload.

I’m also in no position to talk about these things. I provide the occasional compiler bug fix, but I’m not the principal driving force behind the compiler. I build tools and libraries with Carp, and see whether it breaks in interesting ways, or try to come up with use cases that don’t yet exist. In other words, I’m just a user.

That still doesn't mean that it's a good idea to enable -XIncoherentInstances, though.

Common Lisp programmers use static typing for gaining speed, not for any kind of added "safety". For safety we have very good package isolation, really strict typing, typecasing, multimethods, conditions and restarts, and the friendly runtime overseeing the code execution like a god and helping the programmer as a good loyal friend would do.

These features exist for expressiveness, not safety reasons. Although it must be noted that these features make it hard to verify the correctness of programs in a modular fashion. Typecasing makes language-enforced abstraction essentially impossible.

> conditions and restarts

These features exist for debuggability, not safety reasons. Safety means ruling out delimited classes of “bad” behaviors by (language) design.

> friendly runtime overseeing the code execution

Now this is a safety feature, but it is only kind of incompatible with the zero-overhead needs of a low-level language.

Rust, on the other hand, could be called Trust. Borrow checker is for everyone.

I could be sure that they used a static analysis tool, for example, if I watched them use it. But that alone is not enough: the static analysis tool has to be sound, and most static analysis tools for C and C++ deliberately aim for less than soundness.

It seems to me that the benefits of static typing only apply to accidental mistakes (e.g. using a pointer to a character as though it were an integer, or a pointer to a struct, or whatever), and thus that a system with deliberately-circumventable static typing is just fine.

Static typing is useful to enforce the integrity of abstractions across large systems. For instance, using (language-enforced) abstract data types, you can confidently say that a 50 KLOC program won't destroy the invariants of a complicated data structure, because the only place where this could hypothetically happen is a 1500 LOC module, and these 1500 LOC have been verified to the death. Elsewhere, the internal representation of this data structure isn't accessible. Before anyone claims this can be done using object-orientation: No. Object-orientation allows the creation of ill-behaved impostors that are indistinguishable from well-behaved objects unless you use expensive dynamic checks or even more expensive whole-program (and hence non-modular) analyses.

Static typing is also useful to enforce the exhaustiveness of case analyses. Disregarding memory safety issues, which are largely a nonproblem in high-level languages, the vast majority of bugs in computer programs arises from failing to identify corner cases or fully comprehend their complexity. Algebraic data types allow you to substitute ad hoc case analyses with induction on datatypes, for which mechanical exhaustiveness checks are possible, and, in fact, actually performed in practice.

Static typing is also useful as an aid to program verification. Program properties of interest can be classified in two groups: safety properties and liveness properties. Safety properties assert that “bad states are never reached”, and are largely covered by type soundness (for non-abstract types) and type abstraction a.k.a. parametricity (for abstract types). Liveness properties assert that “good states are eventually reached”, and, while types provide less support for verifying liveness properties than safety ones, at least induction on datatypes provides a easy-to-use tool to verify that non-concurrent (but possibly parallel) algorithms will terminate.

All of these benefits fly out of the window if static typing can be circumvented.