Hacker News
points by nanolith 3 days ago | 0 comments
> I don't think that contracts would fundamentally change this.

On their own, no. What contracts provide are annotations for how the programmer expects the code to behave, which can be verified by model checkers or automatic theorem provers. These can already verify memory safety properties; borrow checking only does a subset of what a model checker can do. To scale model checking up so it can work on a large codebase, compositional verification is required. Contracts enable compositional verification, which in turn allows developers to write code safer than what is possible with vanilla Rust or Java.

I do this today with C. The model checked C I write is safer than software written in Rust without a model checker. It is memory safe, and it is verified to work within the specification that I have designed. As far as the specification is correct, it is correct.

We can't rewrite the world in Rust. There are many billions of lines of code in C and C++ that aren't going away. Instead, we need to find ways of making this code safe with as little change to it as possible.

Aún no hay comentarios.