Bend

In de post-AGI-economie zullen mensen uiteindelijk stoppen met het schrijven en lezen van code, maar we hebben nog steeds een eenduidige manier nodig om de AI's die de wereld om ons heen bouwen te vertellen wat er moet gebeuren. Met 'laws' (wetten) kunnen onze intenties veel preciezer zijn dan in natuurlijke taal. Met 'proofs' (bewijzen) kunnen we verifiëren dat de AI onze prompts correct heeft geïmplementeerd. En een snelle compiler zorgt ervoor dat het met hoge snelheid wordt uitgevoerd. Dat is Bend – en niets anders.

1. Bend is SNEL

Bend compileert naar native code. Op één core draait het bijna zo snel als C. Hetzelfde binary draait ook op zestien cores, of op de GPU, waardoor het tot honderd keer sneller kan draaien dan op één core.

(Apple M4 Max · lager is beter)

2. Bend compileert SNEL

De type-checker van Bend is een bewijs-checker (proof checker), vergelijkbaar met die in Lean en Rocq. Bij middelgrote codebases kunnen die processen minuten duren. Bend doet er maximaal een seconde over, zodat een AI-agent na elke wijziging een controle kan uitvoeren.

(Apple M4 Max · lager is beter)

3. Bend is PARALLEL

Geen threads, geen locks en geen kernels die geschreven moeten worden. Splits het werk in tweeën en Bend verspreidt de aanroepen over elke core die het kan vinden, om ze vervolgens weer samen te voegen. Een voorbeeld hiervan is de uitvoering van pow2 op 4.096 GPU-cores.

(pow2.bend draaiend op de GPU)

4. Bend BLOKKEERT fouten – met bewijs

Hoe kun je code vertrouwen die je nooit hebt gelezen? Door een bewijs te eisen. In LAWS.bend declareer je de wetten. Vanaf dat moment kan geen enkele AI een regel code leveren die deze wetten overtreedt.

Kijk hoe het een spel bewaakt: Wet: winnen is onmogelijk

Tot nu toe werkt het!

Nieuwe feature: "Claude, zorg dat het bord omvouwt (wrap around)"

  • Zonder LAWS.bend: Wetten geschonden. AI-fout: gemerged.
  • Met LAWS.bend: Wetten intact. AI-fout: geblokkeerd!

Zonder LAWS.bend zou de bug live zijn gegaan. Met LAWS.bend moest de AI het opnieuw proberen totdat hij een muur bouwde en bewees dat de wet standhield. Het mergen van een bug is wiskundig onmogelijk: het is een theorema.

Voorbeeld: LAWS.bend

# LAW: geen enkele reeks zetten leidt tot overwinning.
law you_cant_win:
for moves: List<Move>            # elke reeks zetten
board = replay(start(), moves)   # afgespeeld vanaf het begin
is_won(board) == False{}         # leidt nooit tot overwinning

Voorbeeld: PROOF.bend

# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... geschreven door de AI

LAWS.bend is een AGENTS.md die wordt ondersteund door bewijs. "Maak geen fouten" is nu type-checked. Ben je sceptisch? Probeer het spel dan maar eens te breken.

5. Aan de slag

5.1 Installatie

curl -fsSL https://bend-lang.com/install.sh | sh

5.2 Je agent instrueren om Bend te gebruiken

Voeg dit toe aan je AGENTS.md:

Wanneer je Bend gebruikt:

  • run bend guide om het te leren
  • gebruik LAWS.bend om belangrijke regels vast te leggen
  • run bend PROOF.bend voordat je commit
  • paralleliseer de code waar mogelijk

Zeg vervolgens simpelweg: "use Bend"!

5.3 Geniet van bugvrije, snelle vibe-coded apps!

Tips: vraag de AI om wetten te schrijven voor alles wat nooit kapot mag gaan, en om alles wat snel moet draaien te paralleliseren. Bend is nog jong: als er iets misgaat, vraag de AI dan om een issue te openen. Bend werkt het beste op de back-end, op Linux en op macOS. Veel plezier! <3

6. Referenties

  • Guide: GUIDE.md bevat de volledige taal; bend guide print deze uit.
  • Paper: BendTT, een affiene afhankelijke typetheorie, de kern van Bend.
  • Paper: BendRT, een parallelle runtime voor CPU's en GPU's, de VM.

Bend is nog in ontwikkeling. Houd rekening met bugs en rapporteer deze a.u.b.