reto

I'm happy to announce Thales, a TypeScript compiler and JS engine in Lean. Thales compiles a subset of TypeScript to Lean via a shallow embedding. I'm building a bridge for TS programmers into Lean's program verification toolset. Check out github.com/jessealama/tha… to get started.

Our AI theorem prover has just got a lot more powerful. Please give it a spin!

AI is writing a growing share of the world's software. No one is formally verifying any of it. New essay: "When AI Writes the World's Software, Who Verifies It?" leodemoura.github.io/blog/2026/02/2…

The CSLib steering committee recently announced the official launch of CSLib — an open-source effort to formalize computer science in Lean, inspired by the impact of Mathlib in mathematics. CS researchers, practitioners, and enthusiasts are invited to get involved to support formalizing essential computer science concepts, and building infrastructure for reasoning about real-world code with Lean. Learn more at: 🌐 cslib.io 📄 White paper: arxiv.org/abs/2602.04846 🤝 Contribute: github.com/leanprover/csl… #LeanLang #LeanProver #CSLib #OpenSource #FormalVerification

I wrote an essay on proof assistants in the age of AI. leodemoura.github.io/blog/2026/02/1…

@sampullara Good times!

@oter i was once at a talk at javaone about ruby and they listed off all the features from smalltalk they have and java doesn't. the response from the crowd was "that was as designed, those features are verboten in real code bases".

don't you hate it when you call a method and obviously should exist and the implementation is straightforward but for some reason the developer forgot to do it? well now you can have claude just write the method just in time!

@sampullara Fun! Come to think of it, Smalltalk’s `doesNotUnderstand` was clearly named with decades of foresight in the context of using it as a similar jump off point to an LLM :-)

Arrived just in time for the weekend 👓… Thanks for putting the work into this @bml_khubbard!

@sgrove The talk was as impressive as the view! Awesome presentation and work!

The view from the office today, putting together some slides for my upcoming talk.

I created a short video about how Arch (the intelligent proxy for agents built on Envoy) can help with intent routing for smarter retrieval, guardrails for safety, and function calling for agent personalization via simple @FastAPIs. Of course, @Gradio is our natively integrated chat interface, and you can select from @MistralAI and @OpenAI LLMs for summarization (more coming soon)

1. Richard Bird, code as poetry. 2. Mike Burrows, absolute mastery of low level code. 3. Jeff Dean, planet-scale coding. 4. Niklas Wirth, frugality and precision in language design. 5. Lennart Augustsson, utter genius at coding anything.

Rust Foundation Collaborates With AWS Initiative to Verify Rust Standard Libraries foundation.rust-lang.org/news/rust-foun…

@satnam6502 Wow!

Greenland, on the way home to California.

I think I'm finally starting to get "virtual ground" with opamps. Trying to work out the max (DAC+opamp) output voltage for the DIY AVR. Aiming for 2Vrms, to match the power amp input(s). With this opamp setup, it will always strive to keep the voltage on both inputs the same.

@justjs14 @beneater Oh wow! Thanks for sharing.

@oter @beneater cool. this looks nice! i also found this, which doesn't look so nice but would be a fun thing to put together. tindie.com/products/hobby…

"The HP-16C could display numbers in Hexadecimal, Decimal, Octal and Binary formats using a standard 7 segment display" hpmuseum.org/hp16.htm

@justjs14 @beneater Swissmicros (not affiliated) makes a successor. I’m happy with mine. The keyboard feels remarkably close to the old originals. swissmicros.com/product/dm16l

i saw @beneater using one of these here and i really want one now. youtube.com/watch?v=gOwi2p…

@satnam6502 @GroqInc Congratulations!

Today is my 3 year anniversary at @GroqInc which has been a fantastic rollercoaster ride involving chip design, formal verification, front-end compiler work, DSLs in Haskell for HW and SW, cool applications and presenting Groq's technology at conferences and universities. It's been a huge hunour to work on such a diverse range of projects, and especially to see how far Groq has come in these three years. Looking inside the engine room of LLMs at Groq, it is utterly fascinating to see all the cogs and wheels that interact with each other to serve these blazingly fast low latency high throughput models. To use some terminology from my previous employer, "exceeds expectations".

@chrismunns Congrats Chris! You made a big difference!

Today was my last day at Amazon/AWS. After 12+ years in total I've decided to take on a new adventure and will be starting my new gig in a few weeks. No badge on laptop photos, no Day 1 quotes. It's been a lot of a lot and im grateful to friends along the way. Cheers!!

@kyleroche @Tesla In another time and space, that would be a “?” email. Wow!

So, @Tesla... I'm purchasing another vehicle (several time repeat customer). I've paid the car in full. I'm getting texts that you'll release the car b/c I don't have a delivery appointment and the app errors that you have no appointments available. Advisor told me to make an appointment. This seems like a pretty hostile customer loop I'm stuck in. @elonmusk I'll always only drive Tesla (different story), but ffs.

Call for talk proposals for TLA+ workshop on April 15th in Seattle, WA, as part of the Linux Foundation Open Source Software Summit North America 2024 (close to 3K crowd) Submit 2 page proposals as explained here by Feb 7th: conf.tlapl.us/home/ #tlaplus RT please!