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.