Halis 1.0.0 发布：让编译器去证明程序安全
来源：dev.to — 2026-11-03
📋 概述
Halis 是一门围绕单一问题设计的系统级语言：如果编译器能证明程序安全，而不是选择相信你，会怎样。它把原本靠 code review 和生产事故发现的问题尽量挪到类型检查器与效果系统里。1.0.0 意味着语言、效果系统与自举流程已经定下来——不是完成，是定稿。
🔑 核心要点
- 没有 null、没有全局变量、没有未初始化值：存在即已初始化。
- 无 GC 的内存安全，移动后使用是编译错误，离开作用域即确定性释放。
- I/O 是声明式效果，共九种；没有 uses 子句的函数就是纯函数，编译器跨整个调用图验证。
- 每一条算术都检查溢出、除零、越界，没有关闭开关；不可信输入被打上污点，未净化无法到达 sink。
💡 金句
“what if the compiler could prove your program is safe instead of trusting you?”
译：如果编译器能证明你的程序是安全的，而不是选择相信你，会怎样？
👍 0
👎 0
← 返回 dev.to 首页