I will talk about Lynx, my Erlang/Elixir to Lean compiler for writing laws and proofs about your Erlang/Elixir programs today at @CodeBEAMio’s lightning talks!

So I was trying to understand why pull requests speeding up the Elixir version were being denied by the clankers while they were being accepted to Go/Express/Rust. It turns out that, not only each project had a different starting point and a different prompt, but also each project also has a different set of verifications that they are required to pass! For example, Elixir is the only guided to "preserve the pinned Rails reference behaviour", the only with a explicit verification that we are using Redis and draining its queue (so we cannot remove it while others can), and the only one actively enforcing it. So it turns out that the people telling you to not read the code cannot even use AI to set up fair benchmarks (probably because they would have to read the code in order to do that). You don't have to believe me, you can do your own research or ask your agent to do it for you. E.g. here is what Claude Code came back with: gist.github.com/josevalim/ae…