[TYPES/announce] ERC project "RustBelt" on foundations for Rust -- Postdoc and PhD positions available!

[Derek Dreyer]

I am very pleased to announce that I have been awarded a 2015 ERC
Consolidator Grant for the project "RustBelt: Logical Foundations for
the Future of Safe Systems Programming".  This 5-year project concerns
the development of rigorous formal foundations for the Rust
programming language.  The project summary appears below.

I am seeking exceptional candidates to fill several postdoc and PhD
positions.  Please see the project web page for more details, and do
not hesitate to contact me if you are interested in joining the
RustBelt team!

Project web page: http://plv.mpi-sws.org/rustbelt/

Best regards,
Derek Dreyer

----------------

Summary of the RustBelt project proposal:

A longstanding question in the design of programming languages is how
to balance safety and control.  C-like languages give programmers
low-level control over resource management at the expense of safety,
whereas Java-like languages give programmers safe high-level
abstractions at the expense of control.

Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom.  As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold.  To rule out
data races and other common programming errors, Rust's core type
system prohibits the aliasing of mutable state, but this is too
restrictive for implementing some low-level data structures.
Consequently, Rust's standard libraries make widespread internal use
of "unsafe" blocks, which enable them to opt out of the type system
when necessary.  The hope is that such "unsafe" code is properly
encapsulated, so that Rust's language-level safety guarantees are
preserved.  But due to Rust's reliance on a weak memory model of
concurrency, along with its bleeding-edge type system, verifying that
Rust and its libraries are actually safe will require fundamental
advances to the state of the art.

In this project, we aim to equip Rust programmers with the first
formal tools for verifying safe encapsulation of "unsafe" code.  Any
realistic languages targeting this domain in the future will encounter
the same problem, so we expect our results to have lasting impact.  To
achieve this goal, we will build on recent breakthrough developments
by the PI and collaborators in concurrent program logics and semantic
models of type systems.