Whiley gets Rusty!

I’ve been learning Rust for a while now but, at the same time, trying to continue developing Whiley. Since Whiley was written entirely in Java, these activities were mutually exclusive and it was frustrating trying to balance things!

Puzzling Strong Updates in Rust

The idea of a strong update comes from earlier work on static analysis and, in particular, pointer analysis. To understand this, let’s imagine a hypothetical non-null analysis for C: int* r = (int*) malloc(sizeof(int)); int** p = &r; At this point, our non-null analysis would conclude that p was nonnull and that r was nullable.

Verifying the Whiley Standard Library

For sometime now, its been possible to use Boogie / Z3 as a backend for verifying Whiley programs. Initially that was pretty sketchy, but it’s really starting to ramp up now.

Fooling the Borrow Checker

An interesting question is how the Rust borrow checker decides when a borrow could still be live. This illustrates a simple example: let mut x = 1234; let z = f(&x); .

Understanding Generic Type Variance (in Whiley)

For languages which support generic types, an important question is deciding whether or not a type C<T> is a subtype of another related type C<S>. Since Whiley was recently extended to support generic types, its interesting to think about how this was handled.