Thread

1. vdombr · 1790714818 · focus · HN ↗

   It's been almost half a year since we got powerful enough models, and I'm wondering, where are all those great things that were created with them? Maybe it's just me, but nothing has changed in my life so far. No improvements, but definitely, I need to be more careful when reading, listening, watching, and using things, as bad quality slowly creeps everywhere.

   1. empath75 · 1790716982 · focus · HN ↗

      I formally proved an important 2025 CS paper (which I did not write) in Lean last month, it took like 2 or 3 weeks of intermittently poking at claude to keep going. AFAIK, it is the first rust-like borrow checker completely formally proven in Lean.

      I'm currently using it as a basis for building a systems language with Rust's memory guarantees, but with new features like generators and co-routines, and effects instead of colored functions. The fact that the borrow checker's properties are formally proven means I can trust more of what Claude is doing than you normally would be able to do.

Unofficial Hacker News client; not affiliated with Y Combinator.