r0ze-at-hn

1. AI Lean is not perfect and AI can easily cheat given it is writing the lean. For anyone playing around with AI Lean code at minimum you need another adversarial prompt to review the ai generated lean.

2. In the paper poking around I see they did re-introduce some bugs to verify it would catch them, but they didn't find any bugs it looks like. Maybe signal is just amazing with many eyes reviewing it, but the real story for the rest of us is that if you start AI converting to Lean the value will be in what assumptions it finds. Even for stuff I thought was really logically tight, Lean found a few minor things I had to fix. Similar to fuzzing where I have never not found bugs when I introduced fuzzing into a codebase I expect the same for converting specs to lean.

3. Having the ability to generate Lean (cheaply) via AI is a very interesting unlock for coding. Potentially being able to go from spec to lean to code, using the lean as a logic gatekeeper has the potential to be a real capability that is used more everyday and not just in research.

And the field is relatively young. Like the other year built a fuzzer with a transformer model as the internal learning engine and other cool stuff like https://antithesis.com

I know fuzzing has been around forever, but it is still surprising how many engineers I encounter who have never used one. I hate fixing bugs and love tools that just find bugs and gave me exact reproducible cases. It was nice to see GoLang get a built in fuzzer to try to help it become more mainstream.

And these days with AI where you need ways it both can't gamify (a unit test that simply returns 'pass') as well as automatic ways to eval generate code fuzzing is a great fit. And not to mention that it is cheaper to fuzz all night than continuously burn tokens looking for ways to crash the code.

The set of who can actually use this is pretty much null as it is. You cannot use it in a publication, nor for any clinical purposes.

The true goal of C++ is the self-preservation and funding of the ISO Committee specification “engine”, while compilers are merely an accidental by-product.

Once you see this then suddenly a lot of odd behavior makes sense. For example the committee can’t break ABI because then the old companies wouldn’t fund the new c++ standard, but would fund a committee that maintains/forks the old thing. The complexity / bureaucracy also provides jobs for those involved in many ways including writing new books every year and or consulting.

While end consumers might really care about compile speed, modularization, security, and all of the things modern languages give, that is secondary to keeping the committee alive.

Younger me would be like, oh no this is horrible someone will fix this! Older me is more sober and understands that once a system is up and running it will continue as is (this being an example of Pournelle’s Iron Law of Bureaucracy). Security by the way of migrations to Rust is causing what the committee sees as the first real threat to its existence as its patrons start adopting more and more Rust. As a result the committee is proposing to break compatibility as a means to keep them around just a little longer. Note: Actually fixing the security issues is not important only giving enough for sponsors to not leave so we will see what actually happens.