Sleight 编程语言仓库发布：带依赖类型与终止检查，实现由 LLM 智能体编写

emmarion 发布了 Sleight 编程语言仓库，语言采用 s-expression 语法、受限依赖类型、每个 binder 标注 multiplicity（erased/many/unique）以及无逃逸的终止检查，编译器会检查程序声明的性能断言如尾调用。仓库含参考实现（OCaml）、自举编译器 slc 和 Lean 4 模型，附千余个测试程序及 checked_runs、no_false、eval_sound 等机器验证定理；palindrom、heapsort、msort 等认证程序中堆排序由 LLM 智能体经多会话写成，2026 年 10 月 14 日的 talk 报告了模型表现。