Software Verificationpalooza

Greg and Rain from the Oxide team joined Bryan and Adam to talk about powerful methods of verifying software: formal methods in the form of TLA+ and property-based testing in the form of the proptest Rust crate. If you care about making software right, don't miss it! In addition to Bryan Cantrill and Adam Leventhal, we were joined by Oxide colleagues Greg Colombo and Rain Paharia.

Some of the topics we hit on, in the order that we hit them:Distributed SagasSteno -- Oxide's implementation of distributed sagasLearn TLA+Hillel Wayne talksHillel Wayne on Alloy 6Quickcheck Paper (2000)Proptest docsRain's example codeuse proptest::prelude::*;

use proptest::collection::vec;

proptest! {

#[test]

fn proptest_my_sort_pairs(input in vec(any::(), 0..128)) {

let output = my_sort(input);

for window in output.windows(2) {

assert!(window[0] <= window[1]);

}

}

#[test]

fn proptest_my_sort_against_bubble_sort(input in vec(any::(), 0..128)) {

let output = my_sort(input.clone());

let bubble_output = bubble_sort(input);

assert_eq!(output, bubble_output);

}

// These proptests implicitly check that my_sort doesn't crash.

}buf-list crateguppy crate... and stay tuned for an upcoming episode revisiting async/await in RustIf we got something wrong or missed something, please file a PR! Our next show will likely be on Monday at 5p Pacific Time on our Discord server; stay tuned to our Mastodon feeds for details, or subscribe to this calendar. We'd love to have you join us, as we always love to hear from new speakers!