Comment by Nezk
4 hours ago
As I understand it, there are no implicit arguments (and, consequently, no unification) here, right? This doesn't seem very serious given the ambitions of a project like this. Of course, one could argue that it isn't necessary if everything is generated by a LLMs, but… why bother with "human-readable" Python-like syntax in that case? It's not Python, after all, and I don't think it would help with LLM code generation in any way.
And benchmarking this language against Isabelle/Agda/Lean/Rocq is strange. The time taken for those systems to perform their checks is mostly spent on elaboration, which includes unification against metavariables, typeclass resolution and tactics. Bend has none of that (there are no type classes or traits, and according to the README, everything must be fully annotated and nothing inferred). This means that the benchmark is comparing Bend's checker to the other systems' elaborators + kernels rather than their kernels (Agda doesn't have this separation though). The latter would be a fairer comparison, and in this area the other systems are already fast. Framing it as "outperforming every proof assistant" without that caveat is misleading.
There is also a problem with LAWS.bend. The typechecker only guarantees that your code satisfies what's written in LAWS.bend — not that LAWS.bend says what you actually meant. There is nothing to stop an LLM from "satisfying" a law with a vacuous or narrower-than-intended formalisation — the trust problem simply shifts from the code to the specification (which could be also generated by LLM, and therefore incorrect). The repository even admits that the compiler itself is 99% LLM generated and not yet fully audited, which seems a questionable basis on which to build a "mathematical guarantees" marketing.