幽灵编程语言

Spectre ​ Spectre 是一种编程语言，用于安全且基于契约的低级系统编程。它允许类型级不变量以及函数级前置条件和后置条件，默认情况下通过使用不变性来实现安全性。本文档旨在充当 Spectre 编程语言的用户指南。为什么？ ​ 明显缺乏基于契约的编程语言来强制执行低级别的正确性。 Spectre 背后的想法是，它默认实现正确性、合理的数据流和不变性，从而使低级编程更加安全，同时防止中断语言及其工具链的便利性和 DX。合约尽可能在编译时进行评估，但是为了避免类似系统（例如 Z3（SMT 求解器））的复杂性，以及与编译器无法证明某些条件为真相关的不便，无法在编译时评估的检查会在运行时自动执行，尽管发布版本中运行时检查的持久性取决于受保护构造的使用。通常通过使用标准库分配器（Arena、Stack）或自定义分配器来手动管理内存以保留低级控制。该语言从高级代码编译为 QBE IR，然后降低为特定于平台的汇编。还有实验性的 LLVM 和 C99 后端。值得注意的是，有一个 –translate-c 功能，允许将 C 代码转换为等效的 Spectre 代码，这对于将现有项目迁移到 Spectre 非常有用。入门​ 简单的 hello world 可以通过以下方式实现： spectre val std = use("std") pub fn main() i32 = { trust std.stdio.print("Hello, world: {d}.", {10}) return 0 } 你会注意到这里的 trust 关键字。任何具有底层不安全机制（例如 std.stdio.print 使用的内置 @print）的操作（例如 IO）都必须显式信任，因为它本质上是不纯粹的。除非您在这些函数周围使用安全包装器，使用前置条件、不变量等……，或者如果您完全使用更简单的函数。例如，没有必要“信任”一个简单的 @puts ，因为除非出现严重的 OOM 错误，否则它不会失败。因此，它在标准库中被标记为安全。前言 ​ 这些文档可能已过时，并且不能保证反映最新的 Spectre API。