NanoLang

我是一种极简的编程语言，专为机器编写、人类阅读而设计。我要求必须编写测试，采用无歧义的语法，并且核心语义经过形式化证明。

当你需要原生性能时，我可以编译成 C 语言；同时，我也提供自己的虚拟机 NanoISA，它将危险的外部调用隔离在独立进程中。我的核心语义使用 Coq 工具，在零公理的基础上进行了机械化证明。

文档

→ 用户指南 ← - 我提供了一个包含可运行示例的教程，建议你从这里开始。

其他资源：

• 快速入门 - 关于我开发环境的简要介绍。
• 快速参考 - 我的语法概览。
• 语言规范 - 我完整的技术定义。
• NanoISA 虚拟机架构 - 我的虚拟机结构说明。
• 形式化验证 - 我的 Coq 证明集。
• 全部文档 - 我所有文档的索引。

快速开始

# 克隆并构建
git clone https://github.com/jordanhubbard/nanolang.git
cd nanolang
make build

# 创建 hello.nano
cat > hello.nano << 'EOF'
fn greet(name: string) -> string {
    return (+ "Hello, " name)
}

shadow greet {
    assert (== (greet "World") "Hello, World")
}

fn main() -> int {
    (println (greet "World"))
    return 0
}

shadow main { assert true }
EOF

# 编译并运行
./bin/nanoc hello.nano -o hello
./hello

BSD 用户： 请使用 gmake 代替 make。

我的特点

• 形式化证明的语义 - 我已在 Coq 中证明了类型安全性、进展性、确定性和语义等价性，且未使用任何公理。
• NanoISA 虚拟机 - 我内置一个基于栈的虚拟机，拥有 178 条指令。它可以将 FFI 调用隔离到子进程中，并能以守护进程方式运行。
• 自动引用计数内存管理（ARC） - 我使用零开销的引用计数机制，无需手动调用 free()。
• 机器主导的优化 - 我会自我剖析并在自动化循环中应用优化策略。此外，在代码生成之前，我还会对抽象语法树进行常量折叠和死代码消除。
• 多目标编译 - 我可以编译成 C 语言以获得原生性能，也可以输出 WebAssembly (--target wasm)、LLVM IR (--target llvm)、PTX/CUDA (--target ptx) 或 RISC-V 汇编 (--target riscv)。每个 WASM 输出都会附带 source map 文件，并可用 Ed25519 签名。
• 代数效应 - 我支持带有类型、可恢复的效应，通过 effect、perform 和 handle 实现。副作用是显式的，并且可以组合使用。
• 异步/等待 - 我会在编译时将 async fn 和 await 降级为 CPS 状态机。
• 双重记法 - 我既支持前缀表示法 (+ a b)，也支持中缀表示法 a + b。我的前缀调用是无歧义的。
• 丰富的模式匹配 - 我支持匹配守卫（Ok(v) if v > 0 =>）、或模式（| A | B =>）、通配符 _，以及穷尽性检查。
• 强制测试 - 如果没有为函数提供 shadow 测试块，我将拒绝编译该函数。
• 类型推断 - 我使用 Hindley-Milner 类型推断算法。当类型明确时，显式注解是可选的（例如 let x = 42）。
• F 字符串和管道操作符 - 我支持 f"Hello, {name}!" 字符串插值，以及 x |> f |> g 管道语法。
• C 互操作性 - 我通过模块与 C 语言通信。为了保护自身，我可以将这些调用隔离到独立进程中。
• VS Code 扩展 - 我提供语言服务器、调试适配器协议服务器，以及打包好的 .vsix 扩展，支持语义高亮、保存时格式化和任务集成。
• Web 演示平台 - 我内置了一个基于浏览器的 CodeMirror 6 编辑器，支持分享永久链接和实时评估。

语言概览

# 变量 — 默认不可变，类型注解在可推断时可省略
let x: int = 42
let y = "hello"            # 类型被推断为 string
let mut counter: int = 0

# 函数必须附带 shadow 测试
fn add(a: int, b: int) -> int {
    return (+ a b)
}

shadow add {
    assert (== (add 2 3) 5)
}

# F 字符串插值
let msg = f"Result: {(add 2 3)}"

# 管道运算符
let result = 5 |> add 3 |> double   # 等价于 double(add(3, 5))

# 控制流
if (> x 0) {
    (println "positive")
}

# 带有守卫和或模式的模式匹配
union Shape { Circle { r: float }, Square { side: float }, Point {} }
match shape {
    Circle(c) if c.r > 0.0 => (println "circle"),
    | Square(_) | Point(_) => (println "other")
}

# 结构体、枚举和泛型类型
struct Point { x: int, y: int }
enum Status { Pending = 0, Active = 1 }
let numbers: List<int> = (List_int_new)
(List_int_push numbers 42)

# 代数效应
effect Log { log : string -> void }
handle (perform Log.log "hi") with {
    Log.log(msg) -> { (println msg) }
}

# 并行绑定提示
par-let a = (compute_x)  b = (compute_y)  in (println (+ a b))

NanoISA 虚拟机

我提供了一种替代 C 语言编译的虚拟机方案。

# 编译为 NanoISA 字节码并运行
./bin/nano_virt hello.nano --run

# 编译为原生二进制文件（嵌入 VM 和字节码）
./bin/nano_virt hello.nano -o hello

# 输出原始 .nvm 字节码，然后单独执行
./bin/nano_virt hello.nano --emit-nvm -o hello.nvm
./bin/nano_vm hello.nvm

# 使用 FFI 隔离运行（外部调用在独立进程中）
./bin/nano_vm --isolate-ffi hello.nvm

架构：

• 178 条指令 - 我采用混合指令集的栈式架构。
• 子进程 FFI (nano_cop) - 我将外部调用运行在独立进程中。即使它们崩溃，我的主程序仍能继续运行。
• VM 守护进程 (nano_vmd) - 我可以作为持久化进程运行，以便更快启动。
• 陷阱模型 - 我将计算与 I/O 分离，这为未来的硬件加速提供了可能。
• 引用计数垃圾回收 - 我以确定性的方式管理内存。当资源超出作用域时，我会释放它们。

我在 docs/NANOISA.md 中详细记录了我的完整架构。

形式化验证

我称之为 NanoCore 的核心语义已在 Coq 中得到机械化证明，且未使用任何公理。

• 类型安全性 - 我已证明类型正确的程序不会陷入僵局。
• 确定性 - 我已证明求值过程只会产生一个结果。
• 语义等价性 - 我已证明我的大步骤语义和小步骤语义是一致的。

我证明的部分涵盖了整数、布尔值、字符串、数组、记录、变体、模式匹配、闭包、递归和可变变量。更多细节请参阅 formal/README.md。

cd formal/ && make    # 构建所有证明（需 Rocq Prover >= 9.0）

IDE与调试器支持

我提供了一个语言服务器（bin/nanolang-lsp）和一个调试适配器（bin/nanolang-dap），用于IDE集成。

make lsp   # 构建 bin/nanolang-lsp  （悬停提示、跳转到定义、补全、诊断）
make dap   # 构建 bin/nanolang-dap  （断点、单步执行、变量检查）

在 editors/vscode/ 目录下提供了一个VS Code扩展，它可以自动连接LSP和DAP服务器。

# 编译为原生C代码（默认）
./bin/nanoc program.nano -o program

# 编译为WebAssembly（生成 program.wasm 和 program.wasm.map 源映射文件）
./bin/nanoc program.nano --target wasm -o program.wasm

# 其他后端
./bin/nanoc program.nano --target llvm  -o program.ll   # LLVM IR
./bin/nanoc program.nano --target ptx   -o program.ptx  # CUDA PTX
./bin/nanoc program.nano --target riscv -o program.s    # RISC-V汇编

# 对WASM模块进行签名和验证
./bin/nanoc sign   program.wasm   # 使用 ~/.nanoc/signing.key 进行签名
./bin/nanoc verify program.wasm   # 验证嵌入的Ed25519签名

# 从三斜杠注释中导出文档
./bin/nanoc program.nano --doc-md -o program.md

构建与测试

make build          # 构建我的编译器（bin/nanoc）
make lsp            # 构建我的语言服务器（bin/nanolang-lsp）
make dap            # 构建我的调试器（bin/nanolang-dap）
make vm             # 构建我的虚拟机后端（bin/nano_virt、bin/nano_vm、bin/nano_cop、bin/nano_vmd）
make test           # 运行我的完整测试套件
make test-vm        # 通过NanoVM后端运行我的测试
make test-quick     # 运行我的快速语言测试
make examples       # 构建我的示例程序

示例与交互式工具

Web Playground（推荐用于学习我的语法）：

./bin/nanoc examples/playground/playground_server.nano -o bin/playground
./bin/playground  # 打开 http://localhost:8080

示例浏览器（需要SDL2）：

cd examples && make launcher

单个示例：

./bin/nanoc examples/language/nl_fibonacci.nano -o fib && ./fib

我的游戏和演示程序已分类整理在 examples/README.md 中。

平台支持

我完全支持以下平台：

• Ubuntu 22.04及以上版本（x86_64、ARM64）
• macOS 14及以上版本（Apple Silicon）
• FreeBSD

Windows： 您可以通过WSL2配合Ubuntu来使用我。

用于LLM训练

我被设计为由机器编写。

• MEMORY.md - 我的模式和惯用法训练参考。
• spec.json - 我的正式规范，以机器可读格式呈现。

贡献说明

对于希望参与贡献的开发者，我在 CONTRIBUTING.md 中提供了相关指南。

许可证

我采用Apache License 2.0许可协议发布。详情请参阅 LICENSE。

NanoLang的真实且毫不夸张的历史

乔丹·哈巴德与雷金纳德·冯·弗拉芬顿三世爵士的持续冒险

连载中的第3部分。← 第2部分：sheme | 第4部分：Aviation → 雷金纳德·冯·弗拉芬顿三世爵士贯穿始终。他并不认可其中任何内容。

此时，这位程序员已经用Bash编写了一个文本编辑器和一个Scheme解释器，并逐渐习惯了那些按理说根本不应该存在的东西。他正坐在书桌前——雷金纳德·冯·弗拉芬顿三世爵士则占据着他最爱的位置：整个键盘——这时，程序员突然冒出一个他自称是“念头”的想法，而雷金纳德爵士则通过强硬地无视它，将其归类为“求救信号”。

“问题在于，”程序员对着房间、对着雷金纳德爵士、也对着他打开的关于形式验证的十七个浏览器标签页说道，“所有我使用的语言都存在歧义。你写f(x)，没人知道这是函数调用还是乘法；你写1 + 2 * 3，居然还会引发争议！更别提那些该被定性为战争罪行的隐式类型转换了。”

雷金纳德眨了眨眼。他以前也听过类似的话。通常，这些话最后都会以某个项目提交到代码库告终。

“我需要一种能由机器编写的语言，”程序员继续说道，“一种没有任何歧义、必须通过测试、并且能够被形式化证明其正确性的语言。”他停顿了一下，脸上浮现出一种仿佛刚刚在现实中找到漏洞的表情。“既然这样的语言并不存在，那我就自己造一个。”

雷金纳德缓缓地、刻意地把一支笔推下了桌面，完全清楚这一举动意味着什么。

接下来发生的一切，后来被程序员称为“必要的”，而雷金纳德则把它归入了“又来了”一类。他们设计了一套语法，无需任何参数就能区分前缀和中缀运算；还制定了一套类型系统，其精确度之高，简直堪比桥梁建造的标准。随后，一台拥有178条指令的操作虚拟机诞生了——程序员称其为“极简”，但数字178却暗示着事实恰恰相反。

“它还需要形式化证明，”程序员在大约第四周时说道，“用Coq来完成，而且不能有任何公理。”

一直趴在形式化规范文档上打盹的雷金纳德，稍微挪动了一下身子，把有关语义等价性的那一节盖了个严实。他早就明白，只要自己赖在那些关键文件上不动，进度就会被拖慢；不过他也清楚，这并不能真正阻止进展，只会让它变得有点湿漉漉罢了。

强制性的测试模块——每定义一个函数就必须配套的“shadow”函数，否则编译器绝不允许继续——之所以加入，是因为程序员如他自己所言：“受够了那些写完就从未测试过、结果也就永远没机会被测试的代码。”当有人问起为何要给测试模块取这样一个奇怪的名字时，程序员回答说：“这个名字很有意境。”至于雷金纳德爵士，则对此不置一词。在他看来，关键字什么的，对买到金枪鱼来说根本无关紧要。

最终，这种语言被命名为NanoLang。它的“极简”程度，就像瑞士手表一样：每个部件都不可或缺，整体尺寸小得超乎想象，而要解释它到底是怎么工作的，所需的时间却远远超过了大多数人的承受范围。

此外，NanoLang还拥有了自己的“声音”。程序员在审阅README文件时注意到，语言在描述自身特性时竟然使用第一人称：“这是因为它本来就是为机器而设计的，机器理应能在不产生歧义的情况下读懂它的文档。”这个说法倒也合情合理，只是听起来仍让人有些毛骨悚然。

雷金纳德从键盘上踱步而过，十四位字符被追加到了类型规范中。后来人们才发现，那串字符原来是jjjjjjjjjkkkk，于是便将其移除了。

形式化证明顺利通过，虚拟机运行正常，编译器甚至成功完成了自编译。程序员久久凝视着这一切，就像凝视着自己亲手做出却真的能运转的东西一样，心中涌起一种特殊的自豪感——这种自豪并非源于优雅，而是源自任务的圆满完成。

“搞定了，”他说。

雷金纳德把桌上的咖啡杯碰翻了——当然不是出于恶意，而是出于一种原则性的拒绝，不愿让程序员独享这份毫无争议的成功时刻。

截至本文撰写之时，NanoLang仅被一个人用于生产环境，而这个人也正是它的作者。雷金纳德爵士依旧对这四个项目一概不予背书，理由包括“程序上的顾虑”、“金枪鱼供应不足”、“弥漫着的狂妄气氛”，以及最近提出的“航空事业”。

NanoLang 快速上手指南

NanoLang 是一门专为“机器编写、人类阅读”设计的极简编程语言。它拥有无歧义的语法、强制的测试机制，并且核心语义已通过 Coq 形式化验证（零公理）。支持编译为 C、WebAssembly、LLVM IR 等多种后端，并提供独立的虚拟机（NanoISA）。

环境准备

系统要求

NanoLang 在以下平台上获得完全支持：

• Linux: Ubuntu 22.04+ (x86_64, ARM64)
• macOS: macOS 14+ (Apple Silicon)
• BSD: FreeBSD
• Windows: 建议通过 WSL2 (Ubuntu) 使用

前置依赖

确保系统已安装以下基础工具：

• git
• make (BSD 用户请使用 gmake)
• C 编译器 (如 gcc 或 clang)，用于构建编译器本身及生成原生代码
• (可选) Rocq Prover (>= 9.0)，仅当你需要构建或验证形式化证明时需要

安装步骤

通过源码克隆并构建项目：

# 克隆仓库
git clone https://github.com/jordanhubbard/nanolang.git
cd nanolang

# 构建编译器及相关工具
make build

注：若需构建语言服务器 (LSP) 或调试器 (DAP)，可分别运行 make lsp 和 make dap。

基本使用

1. 创建第一个程序

创建一个名为 hello.nano 的文件。NanoLang 强制要求为每个函数提供 shadow 测试块。

cat > hello.nano << 'EOF'
fn greet(name: string) -> string {
    return (+ "Hello, " name)
}

// 强制测试块：验证函数行为
shadow greet {
    assert (== (greet "World") "Hello, World")
}

fn main() -> int {
    (println (greet "World"))
    return 0
}

// main 函数也需要测试占位
shadow main { assert true }
EOF

2. 编译与运行

使用 nanoc 将代码编译为原生二进制文件并执行：

# 编译
./bin/nanoc hello.nano -o hello

# 运行
./hello

预期输出：

Hello, World

3. 使用虚拟机模式 (可选)

如果不希望编译为原生代码，也可以直接在 NanoISA 虚拟机上运行：

# 直接运行源码
./bin/nano_virt hello.nano --run

# 或编译为包含 VM 的独立二进制文件
./bin/nano_virt hello.nano -o hello_vm
./hello_vm

4. 其他编译目标

NanoLang 支持多目标编译，例如生成 WebAssembly：

# 编译为 WebAssembly (同时生成 source map)
./bin/nanoc hello.nano --target wasm -o hello.wasm