Bend 2 write-up questions a proof-carrying language with an AI-written compiler

Sources: write-up, Bend repository, HN discussion, second thread
Summary: The post argues that building a language and its compiler by prompting left Bend's author unaware of formal verification as an existing field with existing tools. It recreates Bend's demo, 58 lines of LAWS.bend plus 442 lines of PROOF.bend, as a short SPARK package, and reports GNATprove discharging it with all checks proved, 12 checks.
Comments: HN commenters pointed at the project's own README, which states the compiler, not the kernel, is 99 percent AI-written and has not been fully audited yet.
Why it matters: The comparison sets a model-generated proof-carrying language against an established verification toolchain that discharges the same obligations in fewer lines.