Spectre 编程语言

# Spectre | Spectre 文档 来源：https://spectre-docs.pages.dev/ Spectre 是一门旨在实现安全且基于契约的底层系统编程的编程语言。 它支持类型级不变量、函数级前置条件和后置条件，并通过默认不可变性来增强安全性。 本文档旨在作为 Spectre 编程语言的用户指南。 ## 为什么？(https://spectre-docs.pages.dev/#why) 目前明显缺乏在底层强制保证正确性的基于契约的编程语言。 Spectre 背后的理念是，它默认提供正确性、合理的数据流和不可变性，从而让底层编程更安全，同时不妨碍语言及其工具链的便利性和开发体验。契约尽可能在编译时求值，但为了避免类似 Z3（SMT 求解器）等系统的复杂性，以及编译器无法证明某些条件为真所带来的不便，无法在编译时求值的检查会自动在运行时执行。不过，运行时检查在发布版本中是否保留取决于是否使用了 `guarded` 构造。 内存管理是手动的，以保留底层控制能力，通常通过使用标准库分配器（Arena、Stack）或自定义分配器实现。 该语言将高级代码编译为 QBE IR，然后再降级为平台相关的汇编。此外，还有实验性的 LLVM 和 C99 后端。特别地，`--translate-c` 功能允许将 C 代码翻译成等效的 Spectre 代码，这对将现有项目迁移到 Spectre 非常有用。 ## 快速入门 (https://spectre-docs.pages.dev/#getting-started) 简单的 Hello World 可以通过以下代码实现： ```spectre val std = use("std") pub fn main() i32 = { trust std.stdio.print("Hello, world: {d}.", {10}) return 0 } ``` 你会注意到这里使用了 `trust` 关键字。任何具有底层不安全机制的操作（如 IO，例如 `std.stdio.print` 使用的 `@print` 内建函数）都必须显式地信任，因为它本质上是不纯的。 除非你使用了这些函数的安全包装器（这些包装器使用了前置条件、不变量等），或者使用了更简单的函数。例如，简单的 `@puts` 不需要“信任”，因为除非发生严重的内存不足错误，否则它不会失败。因此，标准库将其标记为安全。 ## 前言 (https://spectre-docs.pages.dev/#foreword) 这些文档可能已过时，不保证反映最新的 Spectre API。