[mattstir]

> Reduce risk of failure through artificial intelligence. CQL contains an embedded automated theorem prover that guarantees the correctness of CQL programs.

Man, it's a rough environment right now marketing-wise. I don't know if they're contractually obligated to say the funny magic words, but the term AI is nearly entirely meaningless at this point. Akin to saying "behold my mighty calculator app: it prevents divisions by zero through artificial intelligence!"

[ianhorn]

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.

[layer8]

I had to read it twice to come to that conclusion. Maybe the prima facie ambiguity is intentional.

[PaulHoule]

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.