Picture Me Coding

In this episode we discuss a couple of recent papers on just-in-time development and agentic systems and how we think they suggest trends that will affect software development for years to come.  We boldly predict that in 2046 people will still not want robot dentists.The Time is Here for Just-in-Time Systems: Challenges and OpportunitiesMDASH: The MS Security Thing Services: The New Software | Sequoia CapitalUnderstanding Spec-Driven-Development: Kiro, spec-kit, and TesslSend us Fan Mail

For the 100th episode of Picture Me Coding we talk about numbers.  Mike talks about his favorite numbers, Erik talks about his favorite ports, and we discuss the surprising phenomenon of Benford's Law.Send us Fan Mail

This week we were joined by our friend Doug Burke, who runs a company and has been working on his "digital life workout partner", a voice-activated LLM tool. Doug's story is interesting because he does not have a background in software development, and we wanted to learn more about what he's building.Send us Fan Mail

In this episode we invite back our friend Bob Farzin to discuss our personal experiences with using teams of agents to write software, and we try to parse out the experiences we're seeing on the interwebs, including Steve Yegge's GasTown and Wes McKinney's discussion of agentic development in the context of Brooks's _Mythical Man Month_."Introducing Beads: A coding agent memory system"Welcome to Gas Town — Steve Yegge's original essayThe Future of Coding Agents — Yegge's follow-upGas Town on GitHub — The actual toolHow to Think About Gas Town — Steve Klabnik's analysisA Day in Gas Town — DoltHub's practical walkthroughGas Town, Beads, and the Rise of Agentic Development — Software Engineering Daily interview with YeggeTop Coding Agents 2025 — Benched.ai comparison guide[April 8, Wes McKinney] AI Agents, The Mythical Agent Month, My Wild AI Coding SetupSend us Fan Mail

In this episode we attempt to explain query optimization and where it came from.  In particular we discuss Patricia Selinger's 1979 SIGMOD paper Access Path Selection in a Relational Database Management System. Access Path Selection paper (PDF)A Conversation with Pat Selinger — ACM Queue (2006)Database Dialogue with Pat Selinger — CACM (2008)Pat Selinger Speaks Out — SIGMOD Interview (PDF)Patricia Selinger — IBM HistorySystem R: Database Research Retrospective — TODS 1981Graefe, G. (1995). The Cascades Framework for Query Optimization Leis et al. (2015). How Good Are Query Optimizers, Really? PVLDB Vol. 9 — introduces the Join Order Benchmark (JOB) and empirically audits modern optimizers.Send us Fan Mail

This week Mike and Erik are joined by Kyle Risse. Erik met Kyle at Scale 23x in Pasadena this year while volunteering for the Tech Team. Kyle has a ton of experience in the field working on networks, infrastructure, linux server operations, and doing stressful operations stuff. In short, he has stories and he was kind enough to come on the show and share them with us!Send us Fan Mail

Some recent articles about research on hash tables made us realize we probably didn't know enough about hash tables, one of the fundamental data structures in the biz.  We talk about the history of hashing and hash tables, and some recent results that overturned a 40 year old conjecture on the most efficient way to insert items.Scientists Find Optimal Balance of Data Storage and Time | Quanta Magazine[2111.00602] On the Optimal Time/Space Tradeoff for Hash TablesSpeeding Up Hash Tables | Communications of the ACMhttps://dl.acm.org/doi/epdf/10.1145/1734714.1734729[2109.04548] Iceberg Hashing: Optimizing Many Hash-Table Criteria at OnceModern Dictionaries by Raymond HettingerFOCS 2024 3B Optimal Bounds for Open Addressing Without ReorderingOptimal Bounds for Open Addressing Without ReorderingSend us Fan Mail

We give a report of our experiences at the 23rd version of the Southern California Linux Expo (Scale 23x) in Pasadena.  Erik was a volunteer in the network group this year, so we have some behind the scenes stories in addition to summaries of interesting talks and sessions.Scale confScale-network repoErik Reinert’s Youtube ChannelDocketBMO and  bmo-agent-setupCline injection attack Adnan KhanDouglas Comer - WikipediaEDB PostgresAdvent of Computing PodcastSend us Fan Mail

In this episode we're joined again by Amy Salley, cohost of the Hugo, Girl! podcast, to help us discuss the Murderbot series of books by Martha Wells.  We discuss our favorite characters and plots, but also how these books touch on AI, consciousness, and neurodivergence.   Galaxy’s Edge Interviews Martha Wells | Author Interview | Sci Fi BlogI didn’t know how non-neurotypical I was until MurderbotWe’re Light-Years Away from True Artificial Intelligence, Says Murderbot Author Martha Wells | Scientific AmericanMartha Wells' next 'Murderbot Diaries' book is 'the family roadtrip from hell on Ringworld' (interview) | SpaceSend us Fan Mail

This episode we look into the history of the web server NGINX and of web servers more generally.  We play myth buster and try to investigate the widespread story that NGINX arose from a need to scale porn sites.Igor Sysoev - WikipediaFree Software Interview with SysoevHistory of ApacheHow Sysoev Ended Up at RamblerSend us Fan Mail

Does anyone program just for fun anymore?  This episode we're talking about recreational programming, with a focus on A.K. Dewdney's Computer Recreations column from the 1980s.  Also, taco shops.https://cs.stanford.edu/~knuth/recreational-cs.pdfFUN 2026The New Turing OmnibusSend us Fan Mail

To celebrate the 50th anniversary of Scheme, we decided to talk about functional programming: what it is, how's it going these days, and does it still matter in the era of AI.  Although there's been 70 years of research into FP it still hasn't become mainstream.  Will AI reverse or accelerate that trend?TIOBE IndexThe Next 700 Programming LanguagesAn Introduction to Functional Programming Through Lambda CalculusSend us Fan Mail

For our first episode of 2026 (and Season 4), we're talking about Amazon's Simple Storage Service (S3).  S3 is probably the biggest cloud service, or at least we think it is, because it is super freakin' huge.  We talk about how it's built, how it works, and how people use it.Building and operating a pretty big storage system called S3How AWS S3 Achieves 1 Petabyte Per Second on Hard Disk DrivesUsing Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3Picture Me Coding 2025 Spotify PlaylistSend us Fan Mail

In this episode we discuss working in the Salesforce environment, and low-code platforms generally, with software engineer Kyle Willcox.  Kyle's dev journey from a CS degree at UNC Wilmington to Salesforce dev to web app developer reveals a lot about both the benefits and pitfalls of working in isolated environments like Salesforce.  Kyle is also a sponsored skimboarder and came to California to ride the surf, so he and Erik nerd out on weather and waves.Low CodeExile SkimboardsSend us Fan Mail

For the holiday we're doing another news roundup, although it's mostly about data centers and AI to be honest.  Inside the Data Centers...Korean Data CenterOracle Data Center DebtCloudflare OutageRust Adoption Drives Android Memory Safety Bugs Below 20%Adversarial PoetrySend us Fan Mail

Erik became fascinated with CRDTs while working on a project, so we're talking about how they work, how they simplify some distributed systems, and how they might protect you from zombies.Conflict-Free Replicated Data TypesA Comprehensive Study of Convergent and Commutative Replicated Data TypesCounters - Aviral GoelSend us Fan Mail

This episode is about the Turing Test, and Alan Turing's original description of the test in Computing Machinery and Intelligence.  We also discuss a recent work by two UCSD researchers that claims that current LLMs pass the Turing Test.Computing Machinery and IntelligenceLarge Language Models Pass the Turing Test Pragmatic Engineer Podcast with Armin RonacherSend us Fan Mail

In 1988 Mark Weiser of Xerox PARC coined the term "ubiquitous computing", and in 1991 he spelled out the particulars of this concept in a Scientific American article called "The Computer for the 21st Century".  We discuss whether or not Weiser's vision was achieved.  It's hard to argue that computers are now all around us, but it doesn't seem like they've faded into the background as Weiser hoped.The Computer for the 21st CenturyDesigning Calm TechnologyToward Ubiquitous Operating Systems: Lessons from the FieldAmbient Computing Has Arrived: Here's What It Looks Like in My HouseSend us Fan Mail

This week we're talking about regular expressions, aka, regex.  These are a favorite tool of programmers, but they also have a dark side.  Do regex cause more problems than they solve?  Can they be evil?  We also discuss the origins of regular expressions, formal language theory, and finite automata.Now You've Got Two ProblemsXKCD: Regular ExpressionsRepresentation of Events in Nerve Nets and Finite AutomataOWASP: ReDOSSend us Fan Mail

A continuation of our discussion about the history of Unix and its development at Bell Labs.  Erik wonders why Unix became successful and which features were novel and important. Mike just wants to talk about cool pranks Group 1127 pulled off.Unix: A History and Memoir - Brian KernighanThe Unix Time-Sharing SystemSend us Fan Mail

This week we talk about the early days of Unix, primarily based on Brian Kernighan's book Unix: A History and Memoir, about his days at Bell Labs and the creation of Unix and C by Ken Thompson, Dennis Ritchie, and other luminaries.https://www.amazon.com/UNIX-History-Memoir-Brian-Kernighan/dp/1695978552https://dsf.berkeley.edu/cs262/unix.pdfhttps://cs3210.cc.gatech.edu/r/unix6.pdfSend us Fan Mail

This week we dip our toes into the river of theoretical computer science and immediately drown.  We discuss the amazing and surprising result of researcher Ryan Williams about how space is a more powerful resource in computing than time.For Algorithms, Memory Is a Far More Powerful Resource Than Time | WIREDhttps://arxiv.org/pdf/2502.17779https://www.youtube.com/watch?v=8JuWdXrCmWgSend us Fan Mail

This week we try to make sense of what were once called "NoSQL" databases, focusing on the early entries into the field like Bigtable, Dynamo and Cassandra.  We try to explain how they differ from prior database systems and what motivated their creation.Bigtable: A Distributed Storage System for Structured DataDynamo: Amazon’s Highly Available Key-value StoreCassandra - A Decentralized Structured Storage SystemSend us Fan Mail

This week we host our friends Bobak Farzin and Kevin Fahey to talk about their experiences building applications with AI tools.  Both Bob and Kevin are very tech savvy in different ways, but neither is a full-time software developer.  Yet both have had good experiences building functional applications with tools like Cursor and Claude Code.  We discuss the benefits and drawbacks of these tools, and the challenges that Bob and Kevin found in building their own software.“Andrej Karpathy: Software Is Changing (Again)”Vibe scraping and vibe coding a schedule app for Open Sauce 2025 entirely on my phone“Will the future of software development run on vibes?” Ars TechnicaSend us Fan Mail

We're talking about databases again.  Or database management systems, we're not totally sure.  In any case, they are relational databases (or database management systems).The relational database has been the go-to system for storing structured data since the 1980s, and is still the most popular type of system to use for applications and business reporting.  We discuss their history, what makes them relational, and our experiences with some of the better known commercial and open-source relational systems.A Relational Model of Shared Databanks - EF CoddDr. Michael Stonebraker - A Short History of Database SystemsSend us Fan Mail

Jim Gray was a key innovator in the area of database technology and he won the Turing Prize in 1998.  He was particularly influential with respect to the definition and formalization of transactions, and he identified and named the A, C, and D of ACID.   Gray, an avid hiker and sailor, disappeared in 2007 while sailing out of San Francisco to the Farallon Islands, and no trace of him was ever found.https://www.microsoft.com/en-us/research/video/behind-the-code-with-jim-gray/https://www.wired.com/2007/07/ff-jimgray-2/Send us Fan Mail

This week Matt Teichman, host of the Elucidations podcast, dropped by the show to chat about functional programming and its surprising relationship to linguistics and philosophy. Matt teaches Linguistics, Philosophy, and Computer Science at the University of Chicago and he also works on open-source software for the University of Chicago library, including an interesting OCaml project used by archivists called Attachment Converter.Thanks to our newest Patreon subscribers: Ralph Minderhoud and Tim Lavoie!Stuff to Check OutMatt's podcast: ElucidationsMatt's website: Matt Teichman - Philosophy - University of ChicagoAttachment Converter, open-source library: Attachment ConverterStanford Encyclopedia of Philosophy entry on Montague SemanticsSend us Fan Mail

In this episode we talk to Jonathan Whitmire who designed the Picture Me Coding swag, logos, artwork (and t-shirts and stickers and coffee mugs!).He gives us a rundown on what it's like working alongside developers and what we talk about when we talk about UX.Send us Fan Mail

This week Mike and Erik talk about the local-first software movement. There's a pretty cool paper about it from 2019 called "Local-First Software:You Own Your Data, in spite of the Cloud", and there's also a podcast, a company, and various projects. Come get inspired to build stuff!Send us Fan Mail

Mike and Erik analyze the tech news again.  The AIs are hallucinating, but gamers are too because of Game Transfer Phenomenon.  The Luddites are back for what's likely a futile effort to keep the robots from taking our jobs, but Mike things he can at least outrun them.Watching These Humanoid Robots Try to Run a Half Marathon Is Hilarious and BizarreProtecting NATS and the integrity of open source: CNCF’s commitment to the community | CNCFGame Transfer PhenomenonHow to Survive the AI Revolution?Yahoo wants to buy ChromeSend us Fan Mail

Today Mike and Erik are joined by John Benson, an attorney with a background in digital forensics who has been at the forefront of integrating LLMs into legal practice. The conversation ranges over the practice of law, digital security, and AIFind out more about John Benson's work here: https://john-benson.com/Send us Fan Mail

This week Mike and Erik tackle Byzantine Fault Tolerance! But what's it all about? Gangsters? Generals? Constantinople? Take a journey with us as we sail off into the dizzying complexity of Byzantine faults.LinksSome constraints and tradeoffs in the design of network communications | Proceedings of the fifth ACM symposium on Operating systems principlesNotes on Data Base Operating SystemsReaching Agreement in the Presence of Faults | Journal of the ACMThe Byzantine Generals Problem - Microsoft ResearchGitHub - JVerwolf/byzantine_generals: An implementation of Leslie Lamport's OM algorithm for the Byzantine Generals ProblemThe Byzantine Generals Strike AgainThe Chinese Generals ProblemSIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft ControlThe Generals – Dean EigenmannPractical Byzantine fault tolerance | Proceedings of the third symposium on Operating systems design and implementationSend us Fan Mail

We have an entertaining and wide-ranging discussion with prominent computer scientist and educator David Beazley, known for his many contributions to the Python community.  We talk about why programming is fun, and how he has created his memorable conference talks and innovative programming classes.  We also touch on music, theater, academic life, and, of course, Dave's No Doubt tribute band.Show Notes:https://www.dabeaz.com/Sans-IO  (https://sans-io.readthedocs.io/)Rust elevator origin story (https://www.technologyreview.com/2023/02/14/1067869/rust-worlds-fastest-growing-programming-language/)Book: "Understanding Software Dynamics", by Richard Sites. Addison-Wesley, 2022. "Critical Program Reading",   https://archive.org/details/youtube-7hdJQkn8rtASend us Fan Mail

In this SCaLE wrap-up Mike and Erik discuss the final day of the conference and talks by Denver Gingerich called "What happens when hardware puts software freedom first? We built a router to find out" and Leslie Lamport titled "Coding isn't Programming", and we got to meet Leslie Lamport and take photos with him and give him Picture Me Coding stickers.Music from #Uppbeat (free for Creators!):https://uppbeat.io/t/night-drift/the-horsemanMusic from #Uppbeat (free for Creators!):https://uppbeat.io/t/night-drift/xMusic from #Uppbeat (free for Creators!):https://uppbeat.io/t/qube/playSend us Fan Mail

This week we are on location in the city of Pasadena, CA for Scale 22x, the Socal Linux Expo. We talked to people and went to talks and drank a lot of coffee. We do a debrief of some of the amazing work we heard about in the first few days of the conference.Stay tuned next week to hear what we learned from Leslie Lamport!Check out some stuff we learned about!- The Open Source Rover (from JPL)- Solomon Hykes Keynote: "Robots Building Robots"Send us Fan Mail

Every once in a while you come across a project where you’re like “Oh, dang, wish I’d thought of that”.   That’s the case with this week’s guest, David R. Morrison.  David is the founder of Applied Computing Research Labs (ACRL), and the creator of Simkube which allows you to record-and-replay Kubernetes simulations.  Recently, he published an article in ACMQueue called "Simulation: An Underutilized Tool in Distributed Systems", which talks about simulation of distributed systems in general and his work with Simkube to analyze two Kubernetes autoscalers: KCA and Karpenter.Links- ACM Queue Article: "Simulation: An Underutilized Tool in Distributed Systems"- Applied Computing Research Labs- Simkube Homepage- Simkube Github Repo- "SimKube: Part 1 - Why do we need a simulator?"- "Autoscaling Mesos Clusters with Clusterman"Send us Fan Mail

This week Mike and Erik are joined by Rob Hernandez who has deep experience with Devops and both cloud and on-prem infrastructure. Rob takes us from the early days of his career as a student IT worker through to consulting for large corporations like Github and finally to running the tech team for the Socal Linux Expo, a massive open-source conference held in Pasadena every year.Speaking of the conference: we're gonna be there! If you want to attend, Rob shared a coupon code with our listeners, which will get you a ticket at half-price. Use the code: FOSS.Find conference info here: https://www.socallinuxexpo.org/scale/22xSend us Fan Mail

This week we continue Mike's origin story for another 20 years of his history and Erik asks him the question: "Where did all the old people go?" Send us Fan Mail

This episode has a bit of everything.  Spaceships! Killer storms! Piracy!  Supercomputers that look like furniture!  But mainly we discover how Mike fell into his lifelong pattern of turning everything into an opportunity to mess around with computers.Send us Fan Mail

In Episode 40 “Agile Trashers Part 2: The Trashening” we mentioned a study titled “268% Higher Failure Rates for Agile Software Projects”. News about this study showed up in all of the usual places (Hacker News, Reddit, TLDR, Google, Slashdot, etc.) and it caused a bit of a stir. That study was published by our guest today, Dr Junade Ali. In this episode we talk about software failure, agile, and what practices might come next.Links“268% Higher Failure Rates for Agile Software Projects”How to Protect Yourself from Killer Computers“So Am I Dr. Frankenstein? Or Were You a Monster the Whole Time?”: Mitigating Software Project Failure With Loss-Aversion-Aware Development Methodologies”Hillel Wayne's criticism“P-Hacking with Dinosaurs”The Strawmen of Agile | HackerNoonSend us Fan Mail

This episode is based on a mild difference in view that Erik and I have about whether it’s useful for programmers to know details of computer hardware.  I feel that it is important and beneficial.  Erik feels... Well, he never did tell me what he really thinks here but I got him to confess that he sometimes solves problems without knowing the reason for the problem in the first place!Send us Fan Mail

Mike and Erik return to the CAP Theorem to finish the discussion started last week. Their goal is to try to find answers to this question: why do software engineers love to talk about the CAP Theorem so much? This episode covers the 2002 Gilbert and Lynch proof of CAP, as well as more recent critiques of the CAP Theorem, mostly based on Martin Kleppeman's article “Please Stop Calling Databases CP OR AP”. LinksBrewer’s “Towards Robust Distributed Systems” (slideshow of the talk!)FLP Paper: Impossibility of Distributed Consensus with One Faulty Process (1985)Lynch:  “A Hundred Impossibility Proofs for Distributed Computing” (1989)Lynch and Gilbert prove CAP Conjecture: “Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services” (2002)Martin Kleppeman “Please Stop Calling Databases CP OR AP” “Highly Available Transactions: Virtues and Limitations”Send us Fan Mail

Your podcast hosts have a suspicion about the CAP Theorem: if you're a working programmer and you've heard of any single result in the field of distributed systems, we think you'll have heard of the CAP Theorem. But did you ever wonder where it comes from? In this episode, we'll tell the story of the CAP Theorem. THERE WILL BE BLUEBERRIES!!!Reach us by email: [email protected] us on Patreon: https://patreon.com/PictureMeCodingLinks2000 PODC website Brewer’s “Towards Robust Distributed Systems” (slideshow of the talk!)FLP Paper: Impossibility of Distributed Consensus with One Faulty Process (1985)Lynch:  “A Hundred Impossibility Proofs for Distributed Computing” (1989)Brewer Interview in 2015: https://medium.com/s-c-a-l-e/google-systems-guru-explains-why-containers-are-the-future-of-computing-87922af2cf95Brewer interview with Software Engineering Daily 2023: https://softwareengineeringdaily.com/2023/05/12/cap-theorem-23-years-later/A Theoretical View of Distributed Systems: Nancy Lynch (2021 Talk)Send us Fan Mail

This week Nathan Mull, a type theorist and CS Professor at Boston University, came on the show to help Mike and Erik understand what the phrase "Propositions as Types" is all about. This is an idea about how programs are connected to logic and mathematical proofs, whether we want them to be or not! You know that program that orders pizza from Dominos?! Yes, even that program is a proof of something. Find out what it proves on this episode of Picture Me Coding!LinksNathan Mull's personal site 2014 Philip Wadler Paper: Propositions as Types2016 Strangeloop Conference recording (Youtube): "Propositions as Types" by Philip WadlerSend us Fan Mail

This week Mike and Erik discussed the work of Frances Allen, who worked for IBM for 45 years starting in 1957. The first female Turing Award winner, Allen authored a number of papers on compiler optimizations that describe techniques that are still in use! Send us Fan Mail

In this episode we looked at the tragic story of tech company CEOs doing drugs and the various knock-on effects.We also played a lightning round of "Aspiring to be a nation state or on drugs?" with various headlines.This is the final episode of Picture Me Coding for 2024 and we’ll be taking a break for a few weeks after this. But we’ll be back next year!Mike made a playlist of all the music we talked about this year too! Find it here: https://open.spotify.com/playlist/6jbM32yzvi8MK3zv2cXPSr?si=f40f8df000404a11REFERENCES ROUNDUPNYT: “The C.E.O.s Are Tripping. Can Psychedelics Help the C-Suite?”The Verge: “Google reveals quantum computing chip with ‘breakthrough’ achievements”Google blog announcement of quantum computing breakthroughScott Aaronson: Shtetl-Optimized » Blog Archive » The Google Willow thingTechCrunch: “Court orders Automattic to restore WP Engine’s access to WordPress.org”Wordpress’s Mullenweg interview with The Verge. Goodbye, unreliable weather forecasts? Google DeepMind's AI model sets new benchmark for 15-day predictions | TechRadar Google Blog: Introducing Gemini 2.0: our new AI model for the agentic erathe Spectator “Are you ready for agentic AI?”Google Genai: new Python repo with “Part” data typeAzure’s AI Agent Service announcementToms Hardware: “AI GPU Clusters with one million GPUs are planned for 2027”Big Tech Embraces Nuclear Power to Fuel AI and Data Centers - IEEE Spectrumhttps://subseacables.blogspot.com/2024/10/breaking-story-facebook-building-subsea.htmlSend us Fan Mail

We carried over from last week and kept doing algos! This week we talked about:- Diffie Hellman- Radix Trees: https://dl.acm.org/doi/pdf/10.1145/321479.321481- Kadane's Algorithm- Raft's Leader Election: https://raft.github.io/raft.pdfSend us Fan Mail

Mike wanted to talk about our favorite algorithms this week, so we covered a few:- Fast Fourier Transforms- HyperloglogSome references are below:- Article in Communications of the ACM: What Is an Algorithm?-  Al-Khwarizmi (mathematician, wikipedia page)-  HyperLogLog Paper: https://algo.inria.fr/flajolet/Publications/FlFuGaMe07.pdfSend us Fan Mail

In this episode, Mike and Erik go back to the topic of time in order to explore what is specifically frustrating to programmers about dealing with time. Why's it so hard and annoying? And why do people get so irritated when we ask them a bunch of questions about what they really want us to build with respect to time?We also mentioned on this and our last episode that there are some new ways to reach out to us (in addition to our email address), but they are:- Bluesky account: https://bsky.app/profile/picturemecoding.bsky.social- Threadless store (in case you want a Picture Me Coding coffee mug or stickers!): https://picturemecoding.threadless.com/- Existing email address: [email protected] us Fan Mail

This week Mike and Erik were trying to understand the arena of formal verification: what are these tools? Where do they come from? How do they work? Can we categorize them?There's a ton of stuff to talk about in this area and we're just learning the things, so we made an attempt here to wade in and figure stuff out!We also mentioned on this episode that there are some new ways to reach out to us (in addition to our email address), but they are:- Bluesky account: https://bsky.app/profile/picturemecoding.bsky.social- Threadless store (in case you want a Picture Me Coding coffee mug or stickers!): https://picturemecoding.threadless.com/ - Existing email address: [email protected] Are Some Links to Stuff We DiscussedLamport’s A Science of Concurrent Programs (pdf)DafnyCloudflare’s Formally Verified DNSP languageWadler’s Propositions as Types paperHillel Wayne’s “Let’s Prove Leftpad” and repoAmazon Science page on “automated reasoning” as an areaAmazon paper “Model checking distributed protocols in Must”Send us Fan Mail