Dmitriy Kashitsyn
Jul 4, 2018 · 7 min read
Image for post
Image for post

Programming is hard.

Not because our hardware is complex, but simply because we’re all humans. Our attention span is limited, our memory is volatile — in other words, we tend to make mistakes.

Computers and software are everywhere: in space, in the air, on the ground, on and even in our bodies. Every day more and more systems are automated and more and more lives depend on software and its quality.

Avionics, self-driving cars, nuclear power plants, traffic control systems, implanted pacemakers. Bugs in such systems almost always endanger human life.

There is a huge difference between “program correctness was checked by tests” and “program correctness was logically proven”. Unfortunately, even if we have a test for every single line of our code, we still cannot be sure that it’s correct. However, having a formal system that would prove our code is correct (at least in some aspects) is another story.

The Rust way

Image for post
Image for post
https://phil-opp.github.io/talk-konstanz-may-2018/#14. Also check out slide #13.

The right part of the chart above shows concurrency and memory safety issues that are fundamentally impossible to get in the safe subset of Rust.

So, just by using Rust they could prevent roughly half of the bugs of that period. Moreover, out-of-bounds access bugs are one of the most dangerous, since they often cause secrets to be compromised, denial of service, and remote code execution vulnerabilities.

Also, it shows that ideas like “one just need to know how to write C” and “just leave low-level stuff to professionals” are not enough. Linux kernel is written by best of the best, top 5% of the industry, and yet, every year, again and again, we get CVEs from the same good ol’ memory bugs.

Surely, those 50 bugs are nothing when compared to millions and millions of lines of working code. But again, life and death problems, remember? When we speak about critical systems, even the tiniest bug may lead to disastrous consequences. Not to mention that these 50 are the bugs that were found. But who knows how many are still there? By using Rust, we know the answer beforehand.

How fast is Rust?

But for Rust it is not the case. All its power comes from its ingenious type system that solves all those issues right at compile time. The very same design that prevents memory issues also prevents data races.

Much like in C++, you only pay for what you use. For example, in Rust you use mutex only when you absolutely need to. Moreover, Rust compiler will force you to use it, so you will never forget to add it.

And all that comes at essentially zero cost. Since most of the checks are performed at compile time, compiled assembly would not be much different from what C or C++ compiler would generate.

For this reason, Rust is now very promising in the fields of embedded electronics, internet of things, and even operating system development — the areas that previously were dominated by C due to high control requirements and strict resource and performance constraints.

Recent versions of Rust even brought SIMD support to the userspace. Previously it was available in nightly releases only, due to API stability constraints. Now you may unleash the full potential of your hardware by using vector instructions either directly or by using convenient wrapper libraries. And even if you don’t plan to do so, the compiler would still auto-vectorize loops and other stuff where possible, in many cases achieving the comparable level of performance as handcrafted vector code.

Why we use Rust

Memory bugs are so hard because you cannot easily write tests to catch them. If you haven’t found a bug during the beta period, then it may stay in the code for years, like a ticking bomb waiting for its hour. Of course, there are tools, like Valgrind, that may help to catch such bugs. But even Valgrind would not catch a bug if the code that it produces wasn’t executed during a debug session, or if it was executed in a way that does not result in a memory issue.

So, by using Rust we eliminate one of the most complex and unpredictable classes of errors.

The role of tests

Image for post
Image for post
https://xkcd.com/221/

And that’s where tests come to play. Tests allow us to check invariants that the compiler could not be aware of. Basically, we need to ensure that a corresponding test covers each result returned and each point in our program where a decision is made. In the examples above, tests must check that function indeed returns the sum of its arguments, and that produced random values are random enough.

In some sense, logic bugs are much easier to deal with. They are, by definition, from the very same domain that a programmer thinks of when writing a program (whereas memory bugs are anywhere but that).

Luckily, we know how to work with such bugs. In the past decades, programmers and computer scientists created a set of methods and tools, by using which we may reduce the amount of logic bugs and keep them at a minimum.

The power of math

Basically, Rust does the very same thing, but for a limited set of issues — specifically, for concurrency and memory safety. Under the hood it uses logic to prove your program is correct in those terms. Think about it, just by writing your normal Rust code, you may have the same level of confidence, as by having a group of mathematicians working on a theorem every time you compile your project.

Unfortunately, proving each and every part of the system is so complex and time-consuming that it’s usually done only for the most critical parts of the software, like an operating system kernel, crypto algorithms, and in some cases, standard library of the language.

For a long time, it was a killer feature of functional programming languages like Haskell to formally prove the code, whereas traditional imperative programming languages remain mostly unprovable, due to extensive use of shared mutability, unsafe pointer arithmetic, and uncontrolled side effects. But Rust can change that, despite being an imperative language, it’s still on its way to being formally proven.

Ralf Jung et al. from the RustBelt project already published some papers that prove that declared fundamental invariants of the Rust language do indeed hold in some important primitives of the standard library.

The thing is, for performance reasons, the Rust standard library contains a lot of potentially unsafe code and raw pointer arithmetic.

In order to prove the correctness of the standard library, Ralf Jung with colleagues designed an approach to unsafety using separation logic and their own calculus that they called λrust. Using that calculus they are trying to prove, that standard library primitives and containers work as intended and that they do not violate the fundamental invariants of Rust. As a byproduct, they had even found a couple of bugs in the synchronization primitives, such as MutexGuard and Arc.

But that work is far from completion. As the author points out:

We have proven far from everything in libstd. That would need way more manpower than we can muster. Instead, we have focused on the libstd primitives that seemed most interesting, and that seemed to stress the type system the most. That’s mostly around interior mutability. As such, we have verified Cell, RefCell, Rc, Mutex, RwLock, Arc and some more individual methods listed in the blog post on the paper.

We hope that someday we’ll be able to bring the same level of correctness proofs to the code written at Parity Technologies.

Combined with its level of control, ability to catch memory and concurrency issues, Rust is becoming one of the most advanced mainstream general purpose languages that may be successfully used to write robust, secure, and efficient programs.


Originally published at paritytech.io on July 3, 2018.

Parity Technologies

powering the decentralised web

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store