Huh, I read the pitch differently. As "reduce risk of (failure through artificial intelligence)," not as "(reduce risk of failure) through artificial intelligence."

Maybe that's my bias since that's what I'm working on, but it's a big benefit to have stronger compiler guarantees of correctness so that an LLM can't screw things up as much. No BSing that it works when the compiler requires proof.

It's what we used to call AI back in the 1970s and 1980s which has advanced a whole lot with little awareness. That is, people thought 10,000 rules was a lot of rules in 1998 and now you can work with 10,000,000 rules. And theorem provers, SAT and SMT all got vastly better.