Dr. David J. Pearce
Verifying the Whiley Standard Library
Wednesday, October 27th, 2021
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.
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.