Bend 2 and the Vibe-Coding Trap
Tension over “vibe-coding” — using LLMs to quickly generate complex systems without deep domain research — is playing out around Bend 2, a new dependently typed language aimed at formal verification and GPU execution. Critics argue the project exemplifies how AI-assisted coding can recreate decades-old ideas with worse trade-offs and misleading marketing, while supporters counter that the author has a long, serious track record in formal methods and made explicit, performance-driven design choices. The exchange highlights broader worries that AI tools can both accelerate experimentation and entrench shallow understanding, raising questions about how much prior art and rigor should be expected before launching ambitious new languages or tools.
Perceptions of “Vibe-Coding” and Prior Research
- Many commenters agree with the article’s core concern: LLMs make it easy to build substantial systems without understanding prior work, which can yield designs decades behind the state of the art.
- Others argue this is not new: developers have always reinvented wheels; LLMs just accelerate the loop and compress the learning phase.
- Several people say they now routinely start projects by using LLMs specifically for prior-art research, but note models often default to “just build it” unless strongly steered.
- Some think the article’s critique applies broadly, but that Bend is a poor example of the problem.
Bend, Formal Verification, and Proof Style
- Central dispute: the article claims Bend’s proof system ignores modern formal verification practice and forces verbose proofs that SMT-based tools could automate.
- Multiple commenters counter that the language is explicitly designed around highly explicit proofs to make proof-checking dramatically faster, accepting verbosity because proofs can be generated by tools/LLMs and are rarely read by humans.
- There is an extended discussion of trade‑offs:
- SMT/automatic tools: concise specs, opaque failures, limited scalability.
- Dependent types / interactive provers: more general, slower, with larger proof scripts.
- Some suggest hybrid approaches (let ATPs solve easy goals, reserve LLMs/manual work for hard parts), and point out existing ecosystems that already mix these techniques.
- Several participants familiar with formal methods say the article mischaracterizes both the field and Bend’s design trade‑offs.
Accuracy and Fairness of the Article
- A major thread criticizes the article as under‑researched and personally unfair: it allegedly infers lack of domain knowledge from lack of keywords (“formal verification”) and then uses that as a morality tale about vibe‑coding.
- After pushback, the article’s author added contextual notes but did not fully retract the original framing; many still find this insufficient or “sleazy,” others see it as a learning moment about tone and implication.
- Some defend strong critique as legitimate; others see it as part of a broader HN “tech drama” / pile‑on dynamic.
Meta: HN, Hype, and Social Dynamics
- Commenters note recurring HN patterns:
- Suspicion of fast‑rising projects (GitHub stars, missing history, “smells botted”).
- Defensive “superfan” responses and appeals to personal credentials.
- Increasing Dunning–Kruger, shallow hot takes, and AI‑driven “slop” projects getting front‑page attention.
- There is both excitement about new verification tools and frustration at discourse quality, with comparisons to past controversial language launches.