Our workshop Languages and Tools for Accelerator Design is next week on March 23. We finally published the schedule over at https://capra.cs.cornell.edu/latte26/, and all the papers are online if you want to start reading already!

Attend on Zoom or in person if you're at ASPLOS this year!

#fpga #asic

@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/

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