Oxide and Friends20 Juni 2023

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 Sagas
Steno -- Oxide's implementation of distributed sagas
Learn TLA+
Hillel Wayne talks
Hillel Wayne on Alloy 6
Quickcheck Paper (2000)
Proptest docs
Rain's example code

use proptest::prelude::*; use proptest::collection::vec; proptest! { #[test] fn proptest_my_sort_pairs(input in vec(any::<u64>(), 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::<u64>(), 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 crate
guppy crate
... and stay tuned for an upcoming episode revisiting async/await in Rust

If 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!

Det här avsnittet är hämtat från ett öppet RSS-flöde och publiceras inte av Podme. Det kan innehålla reklam.

Avsnitt(180)

This Old Repo: LLMs and the Restoration of BattleTris

Bryan and Adam discuss the process of restoring a software project--BattleTris--untouched and unbuilt in over 20 years! How did LLMs help restore code Bryan started in the mid-1990s and what does that...

9 Juni 1h 18min

Rooting for the Home Team with Paul Freedman and Bryan Carmel

Two years ago we introduced listeners to the Oakland Ballers, the startup returning baseball to the city of Oakland. Bryan and Adam were joined again by Paul Freedman and Bryan Carmel to discuss the B...

27 Maj 1h 2min

The Tale of Reverso

Oxide ships a rack scale system--how to test the manufacturing of the backplane and switches? Previously we've been using a collection of sacrificial servers, but this was unwieldy, expensive, and uns...

16 Maj 1h 6min

AI in Computer Science Education

AI is an existential topic for all aspects of education--for none more so than Computer Science. Bryan and Adam were joined by Kathi Fisler and Shriram Krishnamurthi, professors of Computer Science at...

10 Maj 1h 29min

Mechanical Engineering at Oxide [chapter images]

Bryan and Adam were joined by members of the Oxide mechanical engineering team to talk the mechanical challenges of building a rack-scale computer, and--in particular--of scaling manufacturing from ju...

7 Maj 1h 24min

Are LLMs Insufficently Lazy?

Brogrammer Garry Tan has been boasting about "writing" tens of thousands of lines of code each day as the paragon of productivity. Is this really the right way to think about building systems? Bryan a...

3 Maj 1h 31min

Building a Quorum of Trust in the Oxide Rack

The Oxide rack contains within it a distributed system that needs to trust itself. But how is this trust built? Bryan and Adam were joined by colleagues Andrew and Finch to explore how Trust Quorum wa...

4 Apr 1h 26min

When Nine Nines Isn't Enough

Bryan and Adam were joined by members of the Oxide team to describe the multi-year search for a mysterious source of hardware failures. All related to an ultra-reliable--and yet still not reliable eno...

18 Mars 1h 24min