{"type":"rich","version":"1.0","provider_name":"Transistor","provider_url":"https://transistor.fm","author_name":"Oxide and Friends","title":"Software Verificationpalooza","html":"<iframe width=\"100%\" height=\"180\" frameborder=\"no\" scrolling=\"no\" seamless src=\"https://share.transistor.fm/e/f1a2ebcb\"></iframe>","width":"100%","height":180,"duration":4900,"description":"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!\nIn addition to Bryan Cantrill and Adam Leventhal, we were joined by Oxide colleagues Greg Colombo and Rain Paharia.\nSome of the topics we hit on, in the order that we hit them:\nDistributed Sagas\nSteno -- Oxide's implementation of distributed sagas\nLearn TLA+\nHillel Wayne talks\nHillel Wayne on Alloy 6\nQuickcheck Paper (2000)\nProptest docs\nRain's example code\nuse proptest::prelude::*;\r\nuse proptest::collection::vec;\r\nproptest! {\r\n    #[test]\r\n    fn proptest_my_sort_pairs(input in vec(any::<u64>(), 0..128)) {\r\n        let output = my_sort(input);\r\n        for window in output.windows(2) {\r\n            assert!(window[0] <= window[1]);\r\n        }\r\n    }\r\n\r\n    #[test]\r\n    fn proptest_my_sort_against_bubble_sort(input in vec(any::<u64>(), 0..128)) {\r\n        let output = my_sort(input.clone());\r\n        let bubble_output = bubble_sort(input);\r\n        assert_eq!(output, bubble_output);\r\n    }\r\n    // These proptests implicitly check that my_sort doesn't crash.\r\n}\nbuf-list crate\nguppy crate\n... and stay tuned for an upcoming episode revisiting async/await in Rust\nIf 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!","thumbnail_url":"https://img.transistorcdn.com/cVYTzMGAZ_7gNn2i7iJYSuWlQOM4wHdJAzEuWrnLo9A/rs:fill:0:0:1/w:400/h:400/q:60/mb:500000/aHR0cHM6Ly9pbWct/dXBsb2FkLXByb2R1/Y3Rpb24udHJhbnNp/c3Rvci5mbS80OGI3/NjA5NWY4Yjc4NzE0/ZGI5ZmMzZmY4MjFi/YThiYy5wbmc.webp","thumbnail_width":300,"thumbnail_height":300}