Projekt Bend 2 od organizace bendlang chce, aby kód napsaný AI agentem neprošel jen testy, ale také kontrolou předem zapsaných pravidel. Do souboru LAWS.bend může vývojář vložit tvrzení, která aplikace nesmí porušit, například že se součet zůstatků vždy rovná nule nebo že hráč neprojde zdí. Při změně kódu má agent dodat odpovídající důkaz v PROOF.bend; kompilátor jej ověří. Projekt tím míří na chyby, které běžné zadání v přirozeném jazyce zachytí až pozdě.
Bend má syntaxi připomínající Python, používá závislé typy a kompiluje do C, Metalu, CUDA nebo JavaScriptu. Paralelní volání označené vykřičníkem může rozdělit výpočet mezi CPU či GPU, pokud jsou dílčí úlohy vyvážené. Vývojáři tak nemusí ručně psát vlákna, zámky ani GPU kernely. Vedle výkonu je ale podstatné, že pravidla nejsou komentářem pro agenta: jsou součástí kontroly programu.
To má praktický smysl hlavně tam, kde tým dokáže přesně pojmenovat neměnné vlastnosti systému. U bankovního zůstatku nebo herní kolize se takové pravidlo zapisuje snáz než neurčité „nic nerozbij“. U vzhledu rozhraní či obchodního rozhodování bude formalizace podstatně hůř uchopitelná. Důkaz také není náhradou za dobré zadání, protože špatně zvolený zákon může ověřit i chování, které nikdo nechce.
Bend 2 je stále mladý jazyk a jeho autoři otevřeně uvádějí dlouhý seznam hranic. Všechny typy se zapisují ručně, chybí type classes i obecný proof search a programy z Bend 1 ani HVM nepřejdou beze změny. Repozitář navíc upozorňuje, že kompilátor ještě nebyl plně auditován a formalizace v Leanu se nemusí přesně shodovat s implementací. Je to tedy spíš materiál pro vývojáře, kteří chtějí experimentovat s ověřovanými pravidly, než hotová pojistka pro libovolný AI projekt.
Zdroje:
