Bend 2 and the Vibe-Coding Trap
Summary
This post critiques Bend's vibe-coding approach and argues that formal verification should accompany high-level design concepts. It demonstrates how a fully verified Ada/SPARK-style model can prove program properties with GNATprove, highlighting the risk of relying on LLM-generated proofs. The piece advocates integrating formal verification early rather than chasing an all-encompassing language with proofs built in.