David J. Pearce (Blog)

Test-Driving the Rust Model Checker (RMC)

Tuesday, October 26th, 2021

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).

Fooling the Borrow Checker

Wednesday, September 1st, 2021

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); .

Sizing Up Types in Rust

Thursday, July 15th, 2021

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.

Understanding Generic Type Variance (in Whiley)

Sunday, March 14th, 2021

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.

Dynamic Cycle Detection for Lock Ordering

Saturday, December 19th, 2020

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!

Automated Testing for Whiley

Wednesday, December 2nd, 2020

Recently, the online editor for Whiley was updated with some new features. Actually, the update represents a complete rewrite of the front-end in Whiley. Obviously, I am very excited about that!

Understanding Partial Moves in Rust

Monday, November 30th, 2020

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.

The Semantics of Semantic Versioning?

Thursday, September 24th, 2020

Semantic versioning is a surprisingly interesting topic when you get into it. Recently, myself and a few colleagues (Patrick & Jens) have been giving it some thought (and we even wrote an essay on it)!

Whiley is Ten Years Old!

Tuesday, September 1st, 2020

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.

Verifying leftPad() in Whiley

Monday, April 23rd, 2018

The leftPad(string,int) function simply pads a string up to a given size by inserted spaces at the beginning. For example, leftPad("hello",8) produces " hello". This little function shot to fame in 2016 when a developer pulled all his modules from NPM, of which one provided the leftPad() functionality.

1
2
3
4
5