Test-Driving the Rust Model Checker (RMC)

The Rust Model Checker (RMC) allows Rust programs to be model checked using the C Bounded Model Checker (CBMC). In essence, RMC is an extension to the Rust compiler which converts Rust’s MIR into the input language of CBMC (GOTO).

Sizing Up Types in Rust

When learning Rust, understanding the difference between statically and dynamically sized types seems critical. There are some good discussions out there already (e.g. here and here). Whilst these explain the mechanics, they didn’t tell me why its done like this in Rust.

Dynamic Cycle Detection for Lock Ordering

Recently, I discovered that an algorithm of mine from a few years back is being used in both TensorFlow and the Abseil C++ library (see here and here). That is of course pretty exciting since they are both widely used libraries!

Understanding Partial Moves in Rust

Recently I’ve been digging into Rust and, whilst it’s a great language on many fronts, I do find lots of hidden complexity. One example which doesn’t get much attention is partial moves.

Whiley is Ten Years Old!

The first commit recorded in the WhileyCompiler repository on Github is dated June 25th, 2010. That means Whiley has been going for just over ten years already! Wow, time sure does fly.