|Oxide - A Simpler Formalized Rust|
|Written by Harry Fairhead|
|Wednesday, 20 March 2019|
Rust is one of the more remarkable new languages that has a reasonably large following. Oxide, an experimental formalized programming language close to source-level Rust, but with fully-annotated types, highlights its special approach to variables and assignment.
What it takes for a language to become a success is a mystery, but new languages pop up all the time, mostly to wither and be ignored. One recent addition that is much more than a reinvention of C or Java, or an academic exercise in lambda calculus, is Rust. It is an open-source language sponsored by Mozilla, but with a fairly wide support community.
It is a low-level language in the sense that it can be used to tackle the sort of program that you might choose C for, but it has features that make it much safer to use. The important point is that the safety comes not from adding runtime checks, or anything similar, but from language innovations that make it more difficult to write incorrect programs. In particular, it tackles the problem of null pointers and threading by introducing the ideas of ownership, borrowing and lifetimes. These bring about a real change in the way that you think about constructing your program. So much so that many programmers used to simpler languages react against Rust and either move back to simpler languages, such as C, or replacements, such as Go.
Unlike Go, Rust is more difficult language to learn and use correct but it really does bring some new things to the table. To quote from the paper:
"The Rust programming language exists at the intersection of low-level “systems” programming and high-level “applications” programming, aiming to empower the programmer with both fine-grained control over memory and performance and high-level abstractions that make software more reliable and quicker to produce. To accomplish this, Rust integrates decades of programming languages research into a production system. Most notably, this includes ideas from linear and ownership types and region-based memory management . Yet, Rust goes beyond prior art in developing a particular discipline that aims to balance both expressivity and usability. Thus, we hold that Rust has something interesting to teach us about making ownership practical for programming."
As I said Rust is special. They also point out the steep learning curve problem:
"Despite its success, Rust has also developed something of a reputation for its complexity among programmers. It’s not uncommon to hear folks exchange tales of fighting the borrow checker after dipping their toes into Rust. It is natural then to wonder if this experience is inevitable. We say not! While there is likely some inherent complexity to a more powerful type system, we feel that the fundamental issue at hand is clearer — namely, learning new semantics is hard."
As one still learning to use Rust I understand what they are getting at, but I don't see it as "fighting the borrow checker", rather trying to learn new way of thinking that the borrow checker enforces.
All I can say is that at the moment it is worth the effort and this is the first language to make me reconsider my years of devotion to C.
Oxide, which has been described in an arxiv paper by Nicholas Matsakis of Mozilla Research and Aaron Weiss, Daniel Patterson, and Amal Ahmed of Northeastern University, is an attempt to find the essence of Rust. The idea is that, by finding a formal expression of Rust's particular semantics, it might be possible to find better ways of presenting it. Reading through the paper you get a deeper understanding of how Rust manages references and lifetimes. I'm not sure that at the end of the day Oxide is preferable to Rust and as soon as you hit the formal semantics then it is for specialists only.
The bottom line seems to be that we have a proof that Oxide is safe and as Oxide is the essence of Rust it too is probably safe.
Give Rust a try, but don't expect it to be an easy transition.
Oxide: The Essence of Rust by Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, Amal Ahmed
or email your comment to: email@example.com
|Last Updated ( Wednesday, 20 March 2019 )|