Carl Kadie
@carlkadie.bsky.social
Ph.D. in CS & ML. Retired Microsoft Research. Volunteer, open-source projects on ML, Genomics, Rust, & Python. Published in Science & Nature.
📖 https://medium.com/@carlmkadie
🔗 https://www.linkedin.com/in/carlk
📷 https://www.instagram.com/carlk3
📖 https://medium.com/@carlmkadie
🔗 https://www.linkedin.com/in/carlk
📷 https://www.instagram.com/carlk3
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
– 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 2)
Nine Rules for Proving (Rust) Algorithms Correct Without Knowing Formal Methods
medium.com
October 28, 2025 at 3:31 PM
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
– 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" 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
medium.com/@carlmkadie/...
#RustLang #AI #OpenAI #FormalVerification #Lean4 #ChatGPT #ClaudeAI
Vibe Validation with Lean, ChatGPT-5, & Claude 4.5 (Part 1)
Nine Rules for Proving (Rust) Algorithms Correct Without Knowing Formal Methods
medium.com
October 21, 2025 at 10:15 PM
"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
medium.com/@carlmkadie/...
#RustLang #AI #OpenAI #FormalVerification #Lean4 #ChatGPT #ClaudeAI
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
Video: www.youtube.com/watch?v=ec-u...
#Rust #RustLang #TuringMachine #BusyBeaver #Algorithms #BigNumbers #Visualization #Programming
How to Optimize Rust for Slowness — by Carl Kadie — Seattle Rust User Group, September 2025
YouTube video by Rust
www.youtube.com
September 29, 2025 at 5:51 PM
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
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)
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.
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 2)
Lessons from Extending RangeSetBlaze to Maps
medium.com
August 21, 2025 at 7:39 PM
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.
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 range-set-blaze to support maps — associate ranges of integer-like keys with values and do fast range operations.
medium.com/@carlmkadie/...
#rust #programming
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
Nine Rules for Generalizing Your Rust Library (Part 1)
Lessons from Extending RangeSetBlaze to Maps
medium.com
August 11, 2025 at 5:56 PM
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
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
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/...
Includes a nod to Jason Kehe's VR “reality check” in WIRED (2014).
medium.com/@carlmkadie/...
The Last to “Discover” America
You don’t know what’s missing from a technology until it works
medium.com
June 5, 2025 at 2:31 PM
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/...
Includes a nod to Jason Kehe's VR “reality check” in WIRED (2014).
medium.com/@carlmkadie/...
Reposted by Carl Kadie
@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.
Nine Pico PIO Wats with Rust (Part 2) | Towards Data Science
Raspberry Pi programmable IO pitfalls illustrated with a musical example
towardsdatascience.com
May 12, 2025 at 1:18 PM
@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.
Reposted by Carl Kadie
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
newsletter.piptrends.com/p/optimize-y...
#python #Programming #PythonProgramming #ai #ml #SoftwareDevelopment #TechNews #OpenSource #DataEngineering
Optimize your Python Program for Slowness, Mutable default arguments and more
with some more interesting news, articles, packages and projects
newsletter.piptrends.com
April 24, 2025 at 3:04 PM
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
newsletter.piptrends.com/p/optimize-y...
#python #Programming #PythonProgramming #ai #ml #SoftwareDevelopment #TechNews #OpenSource #DataEngineering
Reposted by Carl Kadie
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
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
towardsdatascience.com
April 22, 2025 at 4:09 PM
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
towardsdatascience.com/how-to-optim...
#python #Programming #PythonProgramming #SoftwareDevelopment #TechNews #OpenSource #DataEngineering
🐍 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
→ Write a short program that finishes after the universe dies.
🔗 towardsdatascience.com/how-to-optim...
@towardsdatascience.com
How to Optimize your Python Program for Slowness | Towards Data Science
Write a short program that finishes after the universe dies
towardsdatascience.com
April 8, 2025 at 6:11 PM
🐍 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
→ Write a short program that finishes after the universe dies.
🔗 towardsdatascience.com/how-to-optim...
@towardsdatascience.com
Reposted by Carl Kadie
@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 Pico PIO Wats with Rust (Part 2) | Towards Data Science
Raspberry Pi programmable IO pitfalls illustrated with a musical example
towardsdatascience.com
April 5, 2025 at 6:18 PM
@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.
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/...
Write tiny programs that run longer than the universe — using loops, Turing machines, and hand-written tetration.
📝 medium.com/@carlmkadie/...
How to Optimize your Rust Program for Slowness
Write a Short Program That Finishes After the Universe Dies
medium.com
April 1, 2025 at 5:20 PM
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/...
Write tiny programs that run longer than the universe — using loops, Turing machines, and hand-written tetration.
📝 medium.com/@carlmkadie/...
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.
AI art, cartoon humor, and the modern condition—now with dog phones.
March 27, 2025 at 3:22 PM
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.
AI art, cartoon humor, and the modern condition—now with dog phones.
Reposted by Carl Kadie
@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 Pico PIO Wats with Rust (Part 2) | Towards Data Science
Raspberry Pi programmable IO pitfalls illustrated with a musical example
towardsdatascience.com
March 15, 2025 at 6:18 PM
@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.
Reposted by Carl Kadie
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.
Nine Rules for Running Rust on WASM WASI | Towards Data Science
Practical Lessons from Porting range-set-blaze to this Container-Like Environment
towardsdatascience.com
March 10, 2025 at 12:34 AM
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.
🚀 9 Rules for Porting Rust to the Browser Talk at Seattle Rust User Group 🦀🌐 @towardsdatascience.com
📺 Watch: www.youtube.com/watch?v=i6da...
📺 Watch: www.youtube.com/watch?v=i6da...
9 Rules for Porting Rust to the Browser — by Carl Kadie — Seattle Rust User Group, January 2025
YouTube video by Rust
www.youtube.com
March 5, 2025 at 6:43 PM
🚀 9 Rules for Porting Rust to the Browser Talk at Seattle Rust User Group 🦀🌐 @towardsdatascience.com
📺 Watch: www.youtube.com/watch?v=i6da...
📺 Watch: www.youtube.com/watch?v=i6da...
Reposted by Carl Kadie
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.
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
towardsdatascience.com
February 28, 2025 at 4:47 PM
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.
🚀 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
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
How Rust & Embassy Shine on Embedded Devices (Part 2)
Insights for Everyone and Nine Rules for Embedded Programmers
medium.com
February 25, 2025 at 4:19 PM
🚀 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
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
🚀 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
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
How Rust & Embassy Shine on Embedded Devices (Part 1)
Insights for Everyone and Nine Rules for Embedded Programmers
medium.com
February 18, 2025 at 3:55 PM
🚀 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
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
Reposted by Carl Kadie
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.
Nine Pico PIO Wats with MicroPython (Part 1)
Raspberry Pi programmable IO pitfalls illustrated with a musical example
towardsdatascience.com
January 24, 2025 at 4:47 PM
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.