Mastodawn

@ilyasergey: "I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells the story of how it went and what it means for the future of PL research."

https://proofsandintuitions.net/2026/03/18/move-borrow-checker-lean/

Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory

I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells the story of how it went and what it means for the future of PL research.

Proofs and Intuitions

mattpd 14h ago

paulette d. koronkevich 16h ago

https://slop.zackg.me/ 😬

Real or Slop? — PL Papers Edition

mattpd 1d ago

Who Watches the Provers?
https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/
New essay by Leonardo de Moura on why Lean's architecture is designed to survive AI pressure.

Who Watches the Provers? — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

mattpd 1d ago

zwarich 1d ago

I'm going to start making occasional posts about the resurrected Dada language (see https://smallcultfollowing.com/babysteps/series/dada/) from Niko Matsakis. It has gradually typed roots, but is now implementing a new borrowing model that is significantly distinct from Rust. I would say that it has much more of an Algol feel, compared to Rust's C++ feel.

To start off with an interesting syntactic choice, Dada makes immutable references the default everywhere, so that using a value mutably requires marking it explicitly with `!`, and transferring ownership requires `.give` e.g. `array!.push(element.give)`.

Dada · baby steps

mattpd 2d ago

Gluon: Explicit Performance
https://www.lei.chat/posts/gluon-explicit-performance/
by Lei Zhang

> Gluon enhances the Triton language and compiler solutions with an additional approach towards GPU kernel programming. It strikes a different balance in the portability and performance spectrum to expose more compiler internals; thus giving developers more explicit controls to reach higher performance ceiling.

mattpd 4d ago

cuTile Rust: a safe, tile-based kernel programming DSL for the Rust programming language
https://github.com/NVlabs/cutile-rs
features a safe host-side API for passing tensors to asynchronously executed kernel functions

mattpd Mar 11

Designing AI Chip Hardware and Software
https://docs.google.com/document/d/1dZ3vF8GE8_gx6tl52sOaUVEPq0ybmai1xvu3uk89_is/view
by Bjarke Hammersholt Roune

mattpd Mar 9

Philip Zucker Mar 9

[New Blog Post] Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping https://www.philipzucker.com/thin1/ #python #logic #math @pigworker

Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping

There was a thread on mastodon recently where Conor Mcbride was discussing some really cool stuff. I think the intent was to get at something more interesting, but this is the first place I’ve seen thinnings explained in a way without too many complex trappings around and it really clicked with me. I think I had a primed mind to see something useful to my current set of problems and solutions there. It unlocked a torrent of ideas related to lambda egraphs and generalized unions finds that I’m quite excited to talk about in the next couple posts.

Hey There Buddo!

mattpd Mar 7

Cutie Fly
https://ianbarber.blog/2026/03/06/cutie-fly/
Nice short post on CuTe Layout Representation and Algebra (and how it can help in compilers), CuTe DSL, and FlyDSL
by Ian Barber

Cutie Fly

The FlashAttention 4 paper is out and is fascinating, you should read it! One of the things that Tri called out on Twitter was that the experience of using a Python-based language (CuteDSL) signifi…

Ian’s Blog

mattpd Mar 6

John Regehr Mar 5

a hefty paper containing lots of great details:

MaxSAT Fuzzing and Delta Debugging

https://www.jair.org/index.php/jair/article/view/19716

@mattpd