Salt 系统语言：Z3 定理证明与 MLIR 代码生成

Salt 将 Z3 定理证明直接集成到编译器中

Salt 是一种系统编程语言，旨在提供关于内存安全和函数契约的数学确定性，而无需垃圾回收器的运行时开销或借用检查器的复杂性。通过将 Microsoft Research 的 Z3 SMT 求解器嵌入到编译过程中，Salt 允许开发者定义 requires() 前置条件和 ensures() 后置条件，并在构建时进行验证。

当 Z3 求解器能够证明条件成立时，相应的运行时检查将被完全省略，从而实现该检查的零指令开销。如果 Z3 发现违规，编译器会报告一个具体的反例。在求解器超时（每个义务的限制为 100ms）的情况下，编译器会退回到发出安全的运行时检查。

高性能架构与 MLIR 代码生成

Salt 通过利用 MLIR (Multi-Level Intermediate Representation)，即驱动 TensorFlow 和 PyTorch 的相同基础设施，实现了与 clang -O3 相当的性能。

自动循环分块 (Automatic Loop Tiling)

通过 MLIR affine dialect，Salt 实现了自动循环分块，而无需手动调整分块大小。这使得计算密集型任务（如通用矩阵乘法）能够以与 C 相当的性能运行。在 Basalt Llama 2 推理引擎（一个仅 600 行的 Salt 实现）中，矩阵乘法通过 affine optimizer 进行分块，以保持高效率。

区域内存模型 (Arena Memory Model)

Salt 使用基于 arena 的内存模型取代了传统的垃圾回收和借用检查。所有分配都发生在特定区域内，并且整个区域会一次性释放。编译器静态地验证没有任何引用会超出其所属的 arena 的生命周期，从而消除了手动调用 free() 或复杂的生命周期注解的需要。

现实世界的实现与基准测试

该语言已被用于构建多个高性能系统，展示了其在不同领域的通用性：

• KeuOS: 一个从零开始用 Salt 编写的微内核，可在 x86 硬件上启动。它具有支持 Chase-Lev work-stealing 的 16 核 SMP，以及一个零陷阱 (zero-trap) socket API。基准测试显示，空系统调用仅需 102 个周期 (比 Linux 快 7.4 倍)，IPC ping-pong 仅需 297 个周期。
• Lettuce: 一个兼容 Redis 的内存数据存储，由 567 行 Salt 代码组成。它利用零拷贝 RESP parser 和 kqueue 事件循环，在测试的并发级别 (1–100 个客户端) 下表现优于 Redis。
• Basalt: 一个 Llama 2 推理引擎，其中每个计算内核都携带一个 Z3 证明，证明数组访问是在边界内的。
• FACET: 一个 2D 渲染引擎，其中每个像素写入都被 Z3 验证为在 framebuffer 内，实现了 457 fps。

在 Apple M4 (macOS ARM64) 上收集的性能数据表明，Salt 在 21 个算法基准测试中的 19 个表现出与 C (clang -O3) 持平或更快的速度。由于 arena 分配模型，分配密集型工作负载（如 HashMaps 和 LRU caches）表现出 2-10 倍的性能提升。

语言的人机工程学与工具链

Salt 引入了几个语法特性，以减少样板代码并提高可读性：

• 管道操作符 (Pipe Operator): |> 操作符允许数据从左向右流动，而 |?> 则传播错误。这取代了 C 中冗长的错误处理模式，或 Rust 中繁琐的 trait-bound 仪式。
• F-strings: 类型安全的字符串格式化，可以在不要求堆分配或格式说明符的情况下嵌入表达式。
• 包管理 (Package Management): sp 工具处理项目创建、构建和依赖管理。它使用内容寻址缓存来确保如果源代码未发生变化，则不会重新构建。安全契约在包边界之间进行验证；如果一个库需要特定的条件，编译器会在下游包的每个调用点进行验证该条件。

技术局限性与社区背景

虽然 Salt 正在展示显著的性能和验证能力，但作者指出，这目前是一个研究性质的项目，而非生产就绪的语言。标准库尚不完整，且 Z3 对字符串和量词的支持是部分的。此外，从 Z3 阶段产生的错误消息有时可能难以理解。

社区讨论已将其与其他形式化验证语言进行对比。例如，SPARK (Ada 的一个子集) 自 1980 年代以来一直将 Z3 用于安全关键型的航空航天和国防项目，并且 Verus 通过 Z3 增强了 Rust 以实现类似的验证目标。批评者指出，当前文档和语言规范缺乏连贯性，且该项目除了主要开发者之外，缺乏广泛的社区测试人员群体。