Bend 2 Language Criticized for Overlooking Formal Verification Principles

Bend 2's Approach to AI-Assisted Coding

Bend 2 is presented as a language for the AI coding era, where humans define "laws," and AI generates implementations and proofs, which a compiler then verifies. The concept aims to combine human-defined rules with AI-driven code generation and validation.

Code Volume for Simple Proofs

A demo on Bend 2's homepage illustrates that stating a simple game rule, such as preventing a player from touching a flag, requires 58 lines of code. Furthermore, the AI-generated proofs for these basic properties necessitate 442 lines of code, indicating a high verbosity for fundamental tasks.

The "Vibe-Coding Trap"

The author identifies a "vibe-coding trap," where developers create substantial solutions without sufficient knowledge of existing fields that offer better approaches. In Bend 2's case, the language's design appears to have overlooked the principles and established practices of formal verification, a field directly relevant to its goals, as the term is absent from its documentation.

Comparison with Formal Verification Tools

To highlight the issue, the article demonstrates how a similar game rule can be implemented using SPARK, an open-source language and compiler for formal verification. This comparison suggests that established formal verification tools can achieve comparable results with potentially less complexity and code, contrasting with Bend 2's current approach.