作者认为编译期依赖类型迟早会进入系统编程语言——C++ 有模板和 constexpr，Rust 有 const generics，Zig 有 comptime，但这些特性要么限制极多，要么根本不成体系。Syl 的思路是用模态类型系统来表达编译期计算，受 András Kovács 的 two-level type theory 和 OxCaml 的规划启发。语言里每个值除类型外还有"模态"，两条轴分别是 staticity（static/dynamic）与 erasure（erased/unerased）：static 表示编译期可知，unerased 表示运行期可知；子模态关系只允许弱化不能强化，所以把 static 声明成 dynamic 合法，反过来报错。静态参数会让函数按值特化，erased 则保证该值不出现在运行时程序里；有依赖性的返回类型自然涌现，而 int、bool 本身只是 type 类型的 erased 值，不需要独立的类型文法。代价是允许一般递归也就放弃了全域性：类型检查可能不判定、也没有 universe 层级，作者用 fuel 上限与 unreachable 关键字来收拾这类问题。