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.

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"

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]

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. https://youtube.com/live/IUIOexOvl3M

Live Lean 4 NES emulator development https://youtube.com/live/tSajD4FGMKY?feature=share

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

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) https://youtu.be/bVxTXu-vlgg

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.)

not mine (but 100% true)

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

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?”

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.

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.

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

I regret to inform you they continue to make games solely for me: https://store.steampowered.com/app/3950130/Database_Detective_Minor_Crimes_Division/

Save 15% on Database Detective: Minor Crimes Division on Steam

Solve criminal cases through the power of SQL queries! Help out the city of Los Zorangeles by becoming a Database Detective in this new (unpaid) work from home opportunity.

store.steampowered.com

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

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

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

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

I'm not saying there aren't risks, but I am saying that in the 1980s there were tons of people who would loudly and angrily insist that if you didn't use a manual transmission you didn't really know how to drive, and they were wrong.

Do I dare make a video about higher-kinded types in Lean 4?

I tend to be pretty laissez-faire about pronunciation as long as you can communicate, but I also believe that people who pronounce the word "salmon" as "SALL'mon" must be destroyed.

New video: Rust for Dilettantes, part 2. https://www.youtube.com/watch?v=q7Em0XQTLCQ

the extent to which the things people write on the internet in 2026 makes me say to myself "Man, it feels good to be a normie" cannot be overstated.

ok hear me out a new movie or tv series adaptation of "The Count of Monte Cristo" but in every scene wherever possible they are eating monte cristo sandwiches.

New #Haskell video: some exercises from Set 15 of the #Haskell MOOC, which is all about Squishy Mappables (formerly known by their old, inferior name of "Applicative Functors") https://www.youtube.com/watch?v=WXahHKqrauI

One completely irrational belief I have is that part of my brain absolutely judges banks and stockbrokers by the standard of "How soon after the end of the month is my statement available?" You're a bank! YOU HAVE ONE JOB.

I'm not gonna lie: the amount of work I've had to do just to get to this point has me extremely unamused.

Interviewer: What’s the best song? 20-year old me: Personal tastes vary widely, the very idea of a “best” song is reductive. Today me: It’s ”Long Season”, by Fishmans. That’s the best song. There’s no other right answer. https://www.youtube.com/watch?v=e6xJozKOPYw

Happy to announce my new #Haskell library, BetterNaming, which at just 5 lines massively improves the ergonomics of the language.