Hacker News new | ask | show | jobs
by yjftsjthsd-h 17 days ago
It seems like the obvious point of tension is that you probably want AI to be constrained to/by some rigor. Rust is good because it enforces some safety measures, but I'm more interested yet in the work to have AI work with lean4 or the like to prove its code is up to spec. But that proof checking is probably in direct conflict with fast compilation.
1 comments

yeah but you dont have to proof check every cycle, anyways rust safety is not the slow step