[catnaroek]

The borrow checker is the reason to use Rust, in spite of its annoyances (clunky syntax, limited type inference, non-interactive programming, long compilation times, etc.), so it's always nice to see someone trying to provide the upsides of Rust without the downsides.

That being said, your website is disappointingly terse regarding how Carp recovers the advantages of Rust in the context of a Lisp derivative. What makes this particularly suspicious is the fact that, in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”.

The main reason why I feel confident that Rust is a safe language isn't just the fact that rustc seems to catch many bugs in practice. That alone wouldn't distinguish it from the countless static analysis tools for C and C++ that have existed for decades. The main reason why, at least in my opinion, Rust is such a trustworthy language in spite of its ginormous complexity, is the fact that its core developers, in particular Niko Matsakis, do a terrific job of communicating the process by which Rust's features are conceived and designed. When you read Matsakis' blog [0], it becomes patently clear that Rust's developers take into account the kind of corner cases that in many other languages are only discovered months or years after the feature has been implemented [1][2].

Other languages that inspire similar confidence in me are:

(0) Standard ML. It has a formal proof of type safety.

(1) Pony. It has a formal proof of type safety.

(2) Haskell, as specified in the Haskell Report (i.e., without the crazy GHC-specific language extensions), because its type system is similar to Standard ML's, and there are no reasons to believe the differences introduce any type safety holes.

(3) OCaml, again without the crazy extensions (GADTs, first-class modules, etc.), for more or less the same reasons as Haskell.

Links:

[0] http://smallcultfollowing.com/babysteps/

[1] http://joyoftypes.blogspot.pe/2012/08/generalizednewtypederi...

[2] http://io.livecode.ch/learn/namin/unsound

[hellerve]

While I do agree with the fact that one of the best features of Rust is the communication, I’d tend to find the comparison of the two a little unfair. Carp is very young and in an entirely different position than Rust.

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.

[catnaroek]

> Carp is very young and in an entirely different position than Rust.

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.

[hellerve]

I’m not sure what you’re trying to tell me here, so maybe this comment is going in the wrong direction entirely:

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.

[eadmund]

> in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”.

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.

[catnaroek]

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

[chc]

All mistakes are accidental. Seldom do people write a line of code thinking, "I'm making a mistake." If your language encourages people to casually write unsafe code, any time you spent on safety guarantees was wasted because those guarantees disappear in all of that code and all of the code that touches it. And that's a lot of space for mistakes.

[Tarean]

I'd argue that even the crazy ghc features are mostly trustable. Virtually every language extension and even a lot of the optimizations are explained in papers - including design tradeoffs, proofs of correctness and interactions with other extensions.

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

[flavio81]

>What makes this particularly suspicious is the fact that, in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”

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.

[catnaroek]

> typecasing, multimethods

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.

[b0rsuk]

Correct me if I'm wrong, but you can't be sure if programmers used a static analysis tool ? Maybe they used it just enough to make sure it compiles ? And if all you get is a binary, you can't even run those tools yourself. That's my problem with the argument: "The language has issues, but you can run static analysis tools" and "it takes some self-discipline". If you take over someone's code, you're back to square one.

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

[catnaroek]

> Correct me if I'm wrong, but you can't be sure if programmers used a static analysis tool?

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.