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. 

rust

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.

rust

More Information

Oxide: The Essence of Rust by Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, Amal Ahmed

Related Articles

Is Rust Really Safe?

Rust Improves Tracing

Rust 2018 Released To Improve Developer Productivity

Rust Survey Revelations

The Rust Programming Language (Book Review)

Rust 1.28 Improves Memory Use

Rust 1.26 Adds Existential Types

Rust 1.24 Adds Reformatter

Rust 1.23 Uses Less Memory

Rust Hits Stable 1.0 - So What?

To be informed about new articles on I Programmer, sign up for our weekly newsletter, subscribe to the RSS feed and follow us on Twitter, Facebook or Linkedin.

 

Banner


AWS Releases Lambda SnapStart For .NET Functions
10/12/2024

Amazon has released new services for AWS Lambda SnapStart,  Amazon's performance optimization that aims to significantly improve the startup time for applications.



Copilot Improves Code Quality
27/11/2024

Findings from GitHub show that code authored with Copilot has increased functionality and improved readability, is of better quality, and receives higher approval rates than code authored without it.

 [ ... ]


More News

espbook

 

Comments




or email your comment to: comments@i-programmer.info

<ASIN:1871962609>

<ASIN:1593278284>

Last Updated ( Wednesday, 20 March 2019 )