Carl Kadie

Vibe Validation with Lean, ChatGPT-5, & Claude 4.5 (Part 2) Nine Rules for Proving (Rust) Algorithms Correct Without Knowing Formal Methods

Formally validating a Rust algorithm without really learning Lean brought surprises:
– AI hid sorrys
– Replaced proofs with axioms
– Produced 4,700 lines for 50 lines of Rust
And it still worked.
Read the story:
medium.com/@carlmkadie/...

#RustLang #LeanProver #AI #FormalVerification

Vibe Validation with Lean, ChatGPT-5, & Claude 4.5 (Part 1) Nine Rules for Proving (Rust) Algorithms Correct Without Knowing Formal Methods

"Vibe Validation" I got AI to prove my Rust algorithm correct with Lean. The good news: it worked. The bad news: it took weeks, $50, and 4,700 lines of proof for 50 lines of code.
medium.com/@carlmkadie/...
#RustLang #AI #OpenAI #FormalVerification #Lean4 #ChatGPT #ClaudeAI

YouTube video by Rust How to Optimize Rust for Slowness — by Carl Kadie — Seattle Rust User Group, September 2025

New talk: Understanding new Busy Beaver/Turing machine results with simple programs and fast visualizations. Even shows how to compute 10↑↑15 in code.
Video: www.youtube.com/watch?v=ec-u...

#Rust #RustLang #TuringMachine #BusyBeaver #Algorithms #BigNumbers #Visualization #Programming

Nine Rules for Generalizing Your Rust Library (Part 2) Lessons from Extending RangeSetBlaze to Maps

Nine Rules for Generalizing Your Rust Library (Part 2)
medium.com/@carlmkadie/...

Surprise: sets alone needed 13 iterators, but maps + sets together ballooned to 45. Looking forward to stable yield for easier iterators — though I wonder if it’ll match hand-written performance.

Nine Rules for Generalizing Your Rust Library (Part 1) Lessons from Extending RangeSetBlaze to Maps

Nine Rules for Generalizing Your Rust Library (Part 1)
Lessons from extending range-set-blaze to support maps — associate ranges of integer-like keys with values and do fast range operations.
medium.com/@carlmkadie/...
#rust #programming

The Last to “Discover” America You don’t know what’s missing from a technology until it works

A short new tech essay: why you want to be the last to discover something, not the first.
Includes a nod to Jason Kehe's VR “reality check” in WIRED (2014).
medium.com/@carlmkadie/...

Nine Pico PIO Wats with Rust (Part 2) | Towards Data Science Raspberry Pi programmable IO pitfalls illustrated with a musical example

@carlkadie.bsky.social goes beyond the basics of PIO. His article provides a deep dive into the intricacies of PIO programming on the Raspberry Pi Pico, revealing the "Wats" and strategies for overcoming them.

Optimize your Python Program for Slowness, Mutable default arguments and more with some more interesting news, articles, packages and projects

This week newsletter will be out in 2 days. Interesting stuff by @carlkadie.bsky.social Vuk Rosić, Federico @trey.io @www.stephendiehl.com covered

newsletter.piptrends.com/p/optimize-y...

#python #Programming #PythonProgramming #ai #ml #SoftwareDevelopment #TechNews #OpenSource #DataEngineering

How to Optimize your Python Program for Slowness | Towards Data Science Write a short program that finishes after the universe dies

In this article, @carlkadie.bsky.social demonstrated how a simple nested loop can create a program that runs longer than the lifetime of the universe.

towardsdatascience.com/how-to-optim...

#python #Programming #PythonProgramming #SoftwareDevelopment #TechNews #OpenSource #DataEngineering

How to Optimize your Python Program for Slowness | Towards Data Science Write a short program that finishes after the universe dies

🐍 Python gets a reputation for being slow. This article? It leans in. How to Optimize Your Python Program for Slowness
→ Write a short program that finishes after the universe dies.
🔗 towardsdatascience.com/how-to-optim...
@towardsdatascience.com

Nine Pico PIO Wats with Rust (Part 2) | Towards Data Science Raspberry Pi programmable IO pitfalls illustrated with a musical example

@carlkadie.bsky.social goes beyond the basics of PIO — mastering the nuances of pin control, conditionals, and debugging. His article provides a deep dive into the intricacies of PIO programming on the Raspberry Pi Pico, revealing the "Wats" and strategies for overcoming them.

How to Optimize your Rust Program for Slowness Write a Short Program That Finishes After the Universe Dies

New article — not April Fools:
Write tiny programs that run longer than the universe — using loops, Turing machines, and hand-written tetration.
📝 medium.com/@carlmkadie/...

a new yorker-style cartoon in which a man is walking his dog, but both are staring at the phones. The dog's phone is held by some kind of brace/harness.

A year ago, I saw a family walking their dog while all staring at phones. I thought: What if the dog had one, too? It seemed like a perfect New Yorker cartoon—except AI tools couldn’t quite pull it off. Now, OpenAI’s new model can.
AI art, cartoon humor, and the modern condition—now with dog phones.

Nine Pico PIO Wats with Rust (Part 2) | Towards Data Science Raspberry Pi programmable IO pitfalls illustrated with a musical example

@carlkadie.bsky.social goes beyond the basics of PIO — mastering the nuances of pin control, conditionals, and debugging. His article provides a deep dive into the intricacies of PIO programming on the Raspberry Pi Pico, revealing the "Wats" and strategies for overcoming them.

Nine Rules for Running Rust on WASM WASI Practical Lessons from Porting range-set-blaze to this Container-Like Environment

That's great! I hope to see more and more useful applications for WASI emerge.
medium.com/towards-data...

Nine Rules for Running Rust on WASM WASI | Towards Data Science Practical Lessons from Porting range-set-blaze to this Container-Like Environment

Run your Rust code anywhere with WASM WASI. This article by @carlkadie.bsky.social provides a practical guide with 9 rules for porting your Rust projects to this container-like environment.

YouTube video by Rust 9 Rules for Porting Rust to the Browser — by Carl Kadie — Seattle Rust User Group, January 2025

🚀 9 Rules for Porting Rust to the Browser Talk at Seattle Rust User Group 🦀🌐 @towardsdatascience.com
📺 Watch: www.youtube.com/watch?v=i6da...

Nine Rules for SIMD Acceleration of Your Rust Code (Part 1) | Towards Data Science General Lessons from Boosting Data Ingestion in the range-set-blaze Crate by 7x

Boost your Rust code by 7x with SIMD. @carlkadie.bsky.social shows you how to apply SIMD techniques to data ingestion and other tasks, with a real-world example from the range-set-blaze crate.

How Rust & Embassy Shine on Embedded Devices (Part 2) Insights for Everyone and Nine Rules for Embedded Programmers

🚀 Part 2 is here! Scale Rust & Embassy beyond simple blinks to layered device abstractions!
We build a multiplexed clock w/ async tasks, modular layers, & no_std/no_alloc—all w/o an OS! 🦀⚡
🔗 Free read: medium.com/@carlmkadie/...
#Rust #Embassy #Embedded #RaspberryPi #Pico #IoT

Yes, "Source: openai.com/dall-e-2/. All other figures from the authors."

How Rust & Embassy Shine on Embedded Devices (Part 1) Insights for Everyone and Nine Rules for Embedded Programmers

🚀 New Article!
How do Rust & Embassy improve embedded programming? 🛠⚡

Brad & I explore async, safety, & virtual devices on Raspberry Pi Pico! Try it on an emulator—no hardware needed!
📖 Read Part 1:
🔗 medium.com/@carlmkadie/...

#Rust #Embassy #Embedded #RaspberryPi #Pico #IoT

Nine Pico PIO Wats with MicroPython (Part 1) Raspberry Pi programmable IO pitfalls illustrated with a musical example

What do JavaScript quirks and Raspberry Pi Pico's PIO have in common? @carlkadie.bsky.social explores the 9 PIO 'Wats' and why they're key to unlocking efficient, custom hardware control.