1. 13
  1. 3

    I may sound bitter, but calling it “memory safety project” seems dishonest and intentionally misleading on the real goal: inject Rust in selected projects.

    I was expecting to see address sanitation, or use of theorem provers and separation logic, but it is not. 😒

    Also, take an fairly big project in Java (a language they deem to be memory safe), run Infer, count the amount of possible NullPointerException, then tell me how it fits the definition of memory safety they are using.

    1. 10

      then tell me how it fits the definition of memory safety they are using.

      There’s a significant, meaningful difference between Java NPE which always leads to program crashing with exception, and C-style undefined behavior, which sometimes leads to remote code execution. This difference exists regardless of definition being used.

      That being said, usefully defining what is “memory safety” is hard! The definition they are using is informal: absence of certain specific memory related bugs. NPEs are certainly memory safe according to their definition. If you get NPE, you don’t actually touch garbage memory.

      I don’t know what would be a more useful definition of memory safety. Formally, memory safety is just type safety, in a sense that “well-typed programs don’t get stuck”, but types&programming languages formalism is not directly translatable to real-world languages, which rarely have full formal semantics.

      1. 5

        Indeed. (Though I disagree with your assessment of java. ‘[D]efinition of memory safety’ is not at all difficult; it’s simple: java is sound. Barring the derived-array-upcast thing.)

        Let’s get the Rustls TLS library ready to replace OpenSSL in as many projects as possible.

        Please don’t. Use project everest’s libraries instead.

        1. 1

          @matklad and @Moonchild, thank you for your clarification on Java and NullPointerException; in fact, their concept of memory safety is restricted to out-of-bounds access and use-after-free, so Java fits their restricted definition of memory safety—but does not include most of the types described at Wikipedia article.

          @matklad, do you have a reference on the formal definition of memory safety?

          @Moonchild, I really liked you cited Project Everest, because when I opened this link, I expected to see exactly something like that. And that is where my disappointment (or “bitterness”, if one prefers) came from.

          1. 2

            The best discussion I know is in http://lucacardelli.name/papers/typesystems.pdf, “Execution errors and safety” section. The key idea is that runtime errors may be trapped or untrapped, and the language is safe if programs accepted by the compiler do not exhibit untrapped errors. That’s the difference between C++ and Java with respect to null pointers: Java traps all attempts at null pointer dereference, while C++ assumes that null pointer dereference can’t happen, and optimizes based on that.