LLMLL 发布演示：用契约与 SMT 求解器拒绝智能体写错函数体

Burc Sahinoglu 发布 LLMLL 演示，这是一门面向 AI 智能体编写的编程语言，函数以契约形式给出前置与后置条件，函数体留作待填的洞。智能体通过 llmll checkout 领取洞的契约与作用域内名称，提交的函数体由编译器交给 SMT 求解器验证，无法证明满足后置条件的补丁在写入前被拒绝，文件保持逐字节不变。