iiinova — where your digital self keeps evolving

peterb @peterb.mathstodon.xyz.ap.brid.gy · 09/10/2026

Dead Ends in Proving: I describe trying to prove a simple property of my emulator in #Lean 4 by writing "For all x..." theorems, rather than by construction. It went poorly! www.youtube.com/watch?v=8ZcyQSfrMzs Thumbnail painting: detail from "The Temptation of St. Anthony" (circa […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 02/10/2026

Chapter 7 of Rustlings is all about structures. I complain more about Rust. What a complainer! Thumbnail painting: Heads Landscape (1928) by Francis Picabia youtu.be/aGU_3i5BYVg

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 29/09/2026

Martin Amis once wrote "It was...a symmetrical convenience—for Stalin—that a true description of the Soviet Union exactly resembled a demented slander of the Soviet Union." So anyway this is a subtweet about the EA / AI community in the Bay Area.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 28/09/2026

How is it possible that Slapp Happy's _Casablanca Moon_ hasn't made it into a TV or movie soundtrack yet? www.youtube.com/watch?v=ppq9t7cWDRg

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 25/09/2026

6502 Opcodes in Lean! I continue porting my NES emulator from Haskell to Lean. In this edited (and much shorter) version of the 4-hour livestream, I muse a bit about syntax and my philosophy of programming. The thumbnail painting is Gisele (1908) by Kees Van Dongen […]

mathstodon.xyz

Original post on mathstodon.xyz

010

peterb @peterb.mathstodon.xyz.ap.brid.gy · 23/09/2026

@juergen_hubert Wouldn't this be a natural consequence of writing the fairy tales down at a time when only nobles or clergy were literate? (I'd imagine that this level of rewriting did not happen as much for oral tales, but I don't know the statistics.)

100

peterb @peterb.mathstodon.xyz.ap.brid.gy · 18/09/2026

New video: Let's Try Chipwits Worlds ChipWits was an incredible 1984 programming game for the Mac (and other platforms), written in Forth, where you programmed robots to accomplish. Recently remade for modern platforms, the creators have now released a demo of Chipwits Worlds where instead of […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 11/09/2026

Today we get into the first chapter of Rustlings that tackles something truly Rust-specific: move semantics. Peter is unimpressed with Rust so far, and also with Rustlings as a didactic tool. Thumbnail painting: "The Execution of Lady Jane Grey" (1833) by Paul Deleroche […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 06/09/2026

My friend Nate is taunting me by posting AI summaries of my video from last year about how I'm ambivalent about AI. (Original video: www.youtube.com/watch?v=oOcLnNLAHek)

In this video (0:09-18:03), the creator, Tea Leaves, reflects on

the rapid evolution of technology and shares personal

experiences regarding the use of Large Language Models

(LLMs) in software development.

Key themes include:

+ Historical Context: Drawing from Alvin Toffler's Future
Shock and James Burke's The Day the Universe Changed,
the creator discusses how accelerating technological change
leads to stress and shifts in how we perceive reality and truth
(0:25-8:45)

« The Personal Conflict: The creator, who values the
aesthetic and personal satisfaction of coding, details a past
struggle to write a parser for a NAND to Tetris assembler
project (6:38-8:54).

« The Turning Point: After an initial failure two years ago, the
creator successfully used an LLM to generate the code for
the parser in one try. This sparked feelings of both
satisfaction and deep apprehension about the speed of Al
advancement (8:57-11:51).

« Future Outlook: The creator contrasts a "bad path," where
users lose the ability to learn and understand fundamentals,
with a "good path," where Al serves as a tool to move human
problem-solving to higher levels of abstraction, similar to
how the printing press transformed the preservation and
democratization of knowledge (15:00-17:08).

010

peterb @peterb.mathstodon.xyz.ap.brid.gy · 06/09/2026

@nelson It's useless and can't do anything right, which is why we must work so hard to convince people that using it is literally fascism.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 06/09/2026

@nelson I was promised that it's all smoke and mirrors.

100

peterb @peterb.mathstodon.xyz.ap.brid.gy · 06/09/2026

@nelson Looking forward to watching people get angry at you for doing a useful thing.

100

peterb @peterb.mathstodon.xyz.ap.brid.gy · 04/09/2026

As part of boot-strapping my NES emulator, I port my 6502 CPU emulator from #Haskell to #Lean. Some architectural changes – some encouraged by the language, and others simply from having a second bite at the apple – are made. Thumbnail painting: La Bohémienne Endormie (1897) by Henri Rousseau […]

mathstodon.xyz

Original post on mathstodon.xyz

012

peterb @peterb.mathstodon.xyz.ap.brid.gy · 30/08/2026

Tragic: through a series of bad decisions I have managed to put the best ink I've ever bought in the worst fountain pen I've ever bought.

130

peterb @peterb.mathstodon.xyz.ap.brid.gy · 28/08/2026

Rust for Dilettantes: Vectors Thumbnail Painting: "Portrait of Bianca degli Utili Maselli and Her Children" (1604) by Lavinia Fontana youtu.be/C97AxzFqfgc

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 23/08/2026

RE: toot.wales/@psu_13/1171447379554449… Excellent thoughts on LLMs/"AI" here. Pete (the other Pete) wrestles directly with the contradiction between "Coding LLMs create real value for individual programmers" and "They're still not a silver bullet" both being true. Everyone's favorite […]

mathstodon.xyz

Original post on mathstodon.xyz

010

peterb @peterb.mathstodon.xyz.ap.brid.gy · 21/08/2026

New video: Porting an NES Emulator to #Lean...playing with Subtypes and Dependent Types I write my very first subtype, which is the entire reason I wanted to try porting this emulator in the first place. We explore 2 different ways of accomplishing "here is some data and the compiler has proven […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 21/08/2026

A small preview of the next few weeks (or months!) of my YouTube channel at www.youtube.com/TeaLeavesProgramming. New videos go public every Friday at 10:30 am; "early access" members get access to all videos when they are posted (so if you're early […] [Original post on mathstodon.xyz]

Screenshot of videos on my channel through October 2.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 17/08/2026

This is, precisely, how I write code.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 16/08/2026

No, seriously, no you may not run these processes on my system. Ever. Go away.

100

peterb @peterb.mathstodon.xyz.ap.brid.gy · 16/08/2026

really love how google chrome will just ask me every few hours "hey i'd like permission to scan all the devices on your network" HEY HOW ABOUT YOU GO FUCK YOURSELF instead.

101

peterb @peterb.mathstodon.xyz.ap.brid.gy · 14/08/2026

New video: Rust for Dilettantes 4. I reach the "primitive types" section of Rustlings. www.youtube.com/watch?v=d4OHrim4Gx0 Listen, I'm going to be honest: learning Rust and Lean at the same time is doing something to my brain. Coming back to Rust after writing code in Lean is like […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 14/08/2026

My contribution to the discourse where people are mad at the idea of "the coding isn't the hard part": As someone who has developed software for 40+ years, writing good, clear English is much, much, much harder than writing code, and it isn't even close.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 07/08/2026

New video: Today I continues looking at porting my Haskell NES emulator to Lean 4, and I focus with laser-like intensity on only one question: is there a graphics library I can use to draw on screen? The answer, unsurprisingly, involves using FFI bindings to a library written in C. Let's look at […]

mathstodon.xyz

Original post on mathstodon.xyz

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 05/08/2026

Yes I am in fact talking about your favorite language(†). † Except Elm. Elm gets a pass because they at least TRIED.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 05/08/2026

75 years of compiler theory and practice and not one instance of a compiler correctly telling you what line the error is actually on.

001

peterb @peterb.mathstodon.xyz.ap.brid.gy · 05/08/2026

My most AI-booster coded opinion is that every compiler (yes, EVERY COMPILER) needs to ship with a small local ML model that runs whenever a compile fails and tells you what the syntax error in your code actually is instead of whatever useless bullshit the compiler's error message contains.

300

peterb @peterb.mathstodon.xyz.ap.brid.gy · 02/08/2026

I'm in love with this "Centered dot as the value waiting to be applied" syntax. It's SO MUCH BETTER than "partially applied argument which comes in any color as long as it's the last argument"

001

peterb @peterb.mathstodon.xyz.ap.brid.gy · 02/08/2026

Restructured the shift operations (ASL, LSR, ROL, ROR) to be a little more Clever™ and streamlined in the Lean 6502 emulator. Lean on the left, Haskell on the right. There's nothing intrinsically lean-specific about this, it's just me having another bite at […] [Original post on mathstodon.xyz]

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 01/08/2026

Porting a Nintendo Emulator from #haskell to #lean4 Today we're porting some of the opcodes/instructions from my Haskell 6502 emulator to Lean 4. youtube.com/live/IUIOexOvl3M

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 01/08/2026

Streamed for about 45 minutes, will probably do some more tomorrow morning, early. I think it's unlikely that this particular streamed content makes it onto the edited videos, so if you're a sicko make sure to catch it live.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 31/07/2026

Not gonna lie, very upset that I understand this code.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 31/07/2026

New Video: Rust for Dilettantes We continue working through Rustlings - in this episode, looking at the "if" section. The thumbnail painting is "Magdalene With The Smoking Flame", by Georges de La Tour (1640) youtu.be/bVxTXu-vlgg

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 30/07/2026

Lean 4 definitely has that FP "There's More Than One Way To Do It" thing that can sometimes be a virtue and can sometimes be a vice. (I'm normally Mr. Verbose Dude, but since there are hundreds of opcodes I will probably go for the terse variant here.)

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 28/07/2026

Lean 4 on the left, Haskell on the right. Defined a few additional helpers for Lean to make it less verbose.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 27/07/2026

My reaction to any programming language introducing macros in chapter 1 of their tutorial is “Oh, so you forgot to actually design your programming language, huh?”

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 25/07/2026

A #lean4 paper cut that I hate: it absolutely kills me that they mixed the fields `val` and `property` on Subtype, so every time i try to use it i go down the dead ends of trying BOTH `value` and `prop` and being wrong.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 24/07/2026

The best David Bowie album, and it is not close, is Scary Monsters (And Super Creeps). I will be taking no questions at this time.

010

peterb @peterb.mathstodon.xyz.ap.brid.gy · 24/07/2026

New video: An NES emulator in a theorem prover???!? youtu.be/3TBUiTS6wyY Thumbnail Painting: "Spear Fishing on Lake Krøderen" (1851) by Hans Gude and Adolph Tidemand

010

peterb @peterb.mathstodon.xyz.ap.brid.gy · 21/07/2026

"sorry" as the undefined value in Lean is MUCH funnier to stub out than Haskell.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 19/07/2026

I regret to inform you I am back on my bullshit.

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 17/07/2026

New video: Haskell for Dilettantes, testing with QuickCheck. www.youtube.com/watch?v=zy6j2zsv_vE

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 13/07/2026

I uploaded the wrong video! Second time is the charm. Rust for Dilettantes - Functions. youtu.be/DlOpvZwu9uA

000

peterb @peterb.mathstodon.xyz.ap.brid.gy · 13/07/2026

@nelson ok hear me out: a coding LLM that is disguised as a compiler. You write your program and then when you call "make" the LLM just silently fixes all the dumb things you did. On some timer (maybe twice a day) it leaves some trivial error in place to show you and you get to fix it yourself […]

mathstodon.xyz

Original post on mathstodon.xyz

000