Bend 2 and the Vibe-Coding Trap
Points and comments are a snapshot, not live.
Vibe-coded formal verification language Bend 2 ignores existing tools like SPARK.
The author argues Bend 2 exemplifies a "vibe-coding trap" where developers build complex systems without surveying existing solutions. Bend requires 58 lines of laws and 442 lines of LLM-generated proofs for a simple game demo. In contrast, the same properties can be verified in SPARK with 12 automatically-proved checks using GNATprove, an existing open-source formal verification tool. The Bend webpage and codebase never mention formal verification, suggesting the author built a language around a field without realizing it already exists.
What commenters are saying
Commenters split on Bend 2's legitimacy. Several criticize its AI-written compiler ("99% AI-written, not fully audited") and linked-list strings as slow. Others defend the design choices as GPU-friendly. A sharp critic of the original launch notes getting emotionally charged, credential-focused responses. Some suspect fake GitHub stars, while others attribute popularity to Bend 1's successful launch (1000+ HN upvotes, YouTube videos with 1M+ views). The git history being recycled from Bend 1 raised further skepticism.