rmichaelthomas/planes
GitHub: rmichaelthomas/planes
Planes 是一种能静态计算程序外部副作用并完整追溯值来源的通用编程语言，内置三实现交叉验证机制。
Stars: 0 | Forks: 0
# Planes
**一种展示其工作过程的通用编程语言。**
询问一个程序能对外部世界做什么，Planes 会计算答案
而无需运行它——每一次网络调用、文件写入和时钟读取，及其目标。
询问一个值从何而来，它会回溯到它进入时的边界。
没有其他通用语言能回答这两个问题。Planes 回答了这两个问题，且两个答案都不被盲目信任：三个独立的实现必须达成一致，而且其中一个是用 Planes 编写的。
```
$ python3 planes.py -e 'x = 5; y = 3; z = x + y; why z'
8 from x (5) + y (3)
$ python3 shapes_cli.py hn.planes
effect surface of hn.planes
network:
ask https://hacker-news.firebaseio.com/v0/item/{...}.json (computed)
ask https://hacker-news.firebaseio.com/v0/topstories.json
file:
write results.json
console:
show found {...} (computed)
show {...} (computed)
```
生成该界面没有进行任何一次网络调用。
## 目录
| | |
|---|---|
| [运行它](#run-it) | 三个实现和一个浏览器 |
| [三个实现](#three-implementations) | 自举带来的好处，以及“达成一致”的含义 |
| [词汇表](#the-vocabulary) | 32 个单词，13 个 builtins，7 种 effect 类型 |
| [语言](#the-language) | 一页纸的语法说明 |
| [数字是精确的](#numbers-are-exact) | 有理数，而非 floats |
| [Effect 表面](#effect-surface) | 程序*能*做什么 |
| [原因](#why) | 值从何而来 |
| [规则](#rules) | 作为表面之上一个平面的治理 |
| [标注](#annotations) | `because` 和 `note`，被证明是惰性的 |
| [错误指明修复方法](#errors-name-the-fix) | 一项承诺，已被统计 |
| [模块](#modules) | 扁平命名，报告冲突 |
| [外部函数](#foreign-functions) | FFI，以及为什么 `doing` 是一项声明 |
| [宿主](#the-host) | 七个方法，别无其他 |
| [机器可读表面](#machine-readable-surfaces) | 作为数据的语法 |
| [布局](#layout) | 什么在什么位置 |
| [门控](#the-gate) | 如何进行检查 |
## 运行它
```
python3 planes.py ordinary.planes # run a program
python3 planes.py money.planes --effects # ...and log what it did
python3 planes.py hn.planes --why avg # ...and explain a value
python3 shapes_cli.py hn.planes # what it CAN do, without running
python3 shapes_cli.py hn.planes --json # machine-readable
python3 shapes_cli.py --diff demo/v1.planes demo/v2.planes
python3 shapes_cli.py demo/rules/violation.planes --rules
node js/cli.mjs run ordinary.planes # the JavaScript implementation
node js/cli.mjs meta run ordinary.planes # ...running the SELF-HOSTED one
open index.html # run and analyse in a browser
open paint.html # ...or paint a program's `show` output onto a canvas
bash scripts/ci.sh # the gate
```
这两个页面也已被托管，无需安装：。
门控需要 `ruff` 和 `mypy`，它们位于 `./.venv` 中。如果缺少它们，它会在第一步告诉你。
## 三个实现
同一种语言，编写了三次。它们不是为了方便而做的移植——
它们就是检查本身。
| | 编写语言 | 是什么 |
|---|---|---|
| `interp.py` + `parser.py` + `lexer.py` | Python | 参考实现 |
| `js/interp.mjs` + `js/parser.mjs` + `js/lexer.mjs` | JavaScript | 第二个宿主，独立编写 |
| `grammar/interp.planes` + `parser.planes` + `lexer.planes` + `json.planes` | **Planes** | 语言自身 |
第三个是最有趣的一个。`grammar/interp.planes` 是用 Planes 编写的 Planes 解释器；它可以在其他两个中的任意一个上运行。
```
$ node js/cli.mjs meta run ordinary.planes
```
那是运行在 JavaScript 上的 Planes 中的 Planes。不涉及 Python。
**“它们达成一致”的含义是经过测量的，而不是断言的。** 一次扫描会通过全部三个实现运行 349 种值形态——每一个 builtin 和 operator 针对每一种值——并比较各自拒绝执行时的 tag、detail 文本和 fix 子句：
```
$ python3 planes.py -e 'x = "5" + 1'
error — cannot-combine: cannot combine "5" with 1 using +
try: convert first — text of n to build text, or number of t to do arithmetic
```
三个实现逐字节地生成了相同的消息。**349 种形态中共有 0 个分歧。** Effect 表面和派生图也是由 JavaScript 栈计算的，因此这两项保证都不依赖于 Python。
## 词汇表
封闭且被断言。整个保留表面有 45 个名称——32 个关键字加上 13 个 builtins——这两个计数都由测试套件锁定，因此添加一个词是一个可见的决定，而不是某种偏移。作为规模对比：Python 有 35 个关键字。这里数量小不是指词汇表，而是[宿主](#the-host)——七个方法，这才是让 effect 表面可计算的根本原因。
**32 个关键字** —— parser 为了了解语句形态而必须看到的仅有词汇：
```
and as doing each else fail false first
for from foreign give if in let not
nothing of or places plus round rule show
to true use when where why with write
```
**13 个 builtins** —— 普通函数，不是关键字，像 `count of xs` 这样调用：
```
ask count join lower normalize number read rest root sine text upper whole
```
`sine` 接受**度数**并为**每一个**参数返回一个近似值，包括 `sine of 0` —— 它的算法在任何参数下都没有精确路径。`root` 是平方根，也是唯一一个由其参数决定精确度的操作：`root of 9` 精确等于 `3`，`root of 2` 是近似的，而负参数会被拒绝，而不是给出一个虚数答案。这些规则，以及为什么两者不同，都在 [`square-root-spec.md`](square-root-spec.md) 中。
`number` 是 `text` 的反方向 —— `number of "12.5"` 是精确的数字 `12.5`。它宁可拒绝也不会去猜测：非数字文本、空字符串、指数表示法，以及带有 `~` 前缀的近似值（该语言自有的标记，表示无法打印某个值的精确形式），都会指明它们各自的错误，而不是返回 `nothing` 或 `0`。
**7 种 effect 类型** —— 可以向宿主请求的封闭词汇表：
```
ask clock env random read show write
```
`clock`、`random` 和 `env` 是*环境相关的* (ambient)：它们使结果依赖于程序外部的某些事物，因此读取时钟的函数不是纯函数。
其他一切都是普通名称。Builtins 是可以被覆盖 (shadowable) 的，并且分析器会遵循覆盖：
```
to word count of phrase: # `count` used freely inside a name
give 42
to read of source: # shadows the builtin entirely
give "no file is touched"
```
一个被覆盖的 `read` 不会执行任何文件 effect，并且表面会如实说明。在名称读起来如同散文的语言中，`count`、`text` 和 `read` 是人们惯用的词汇。
**两种调用形式，刻意设计得不同：**
- `f of x` 紧密绑定 —— `double of 5 + 1` 是 `(double of 5) + 1`
- `f x` 接受整个表达式 —— `ask "https://" + text of n` 是一次调用
将它们理解为“将此应用于那一个事物”与“将此应用于随后的所有内容”。
## 语言
```
use http # declare a module before its effects work
use file
x = 5 # binding; `let` optional
xs = [1, 2, 3] # lists
r = { name: "Ada", score: 450 } # records
name = r.name # dot access
r2 = r with score: 500 # record update — a new record
ys = xs plus 4 # list append — a new list
to add of a, b: # function definition
give a + b # return
to fetch stories: # multi-word name, no arguments
give first 30 of everything
r = add of 2, 3 # call; `of` binds tightly
r = add(2, 3) # equivalent
ys = for each x in xs: x * 2 # comprehension
zs = for each x in xs where x > 2: x # with filter
if n > 50: # conditional
show "big"
else:
show "small"
when user is { role: "admin" }: # match on a record's SHAPE
give true
else:
give false
when e is { path }: # bind a field by name
show text of (count of path)
count of xs # builtins
text of n
join of ["a", "b"]
body = ask "https://..." # network round-trip, needs `use http`
or fail as api-down # rename any failure to a domain error
x = risky() or fail as e: # ...or catch it, as an ordinary record
show e.tag
show e.detail
show e.fix
fail "the order is empty" as empty-order # raise one yourself
fail { message: "...", fix: "add a line" } as t # ...naming the fix
write xs to "out.json" # file write, needs `use file`
why total # derivation query
```
**被捕获的错误是一个普通 record**，通过形态而不是类型来区分：`{ tag, detail, fix, path }`。这四个字段总是存在，当它们不适用时为 `nothing` —— 因为缺失的字段在 `when` 下无法匹配，所以如果某个字段不存在，将会导致 `when e is { fix }:` 静默跳过每一个没有指明 fix 的错误。
## 数字是精确的
`0.1 + 0.2` 是 `0.3`。`1 / 3` 是三分之一。`9007199254740993 * 2` 是精确的。
```
$ python3 planes.py money.planes
subtotal 59.97
tax 4.947525
total 64.917525
due 64.92
```
数字是精确的有理数 —— 不是 floats，也不是 `Decimal`。原因是 `why`：包含静默舍入步骤的派生回答的是关于答案的问题，而不是关于程序的问题。Floats 几乎在每次运算时都会舍入；Decimal 在除法时会舍入。精确的有理数从不舍入，因此 `why` 报告的是实际发生的算术运算。
| | float | Planes |
|---|---|---|
| `0.1 + 0.2 == 0.3` | false | true |
| `round 2.675 to 2 places` | 2.67 | 2.68 |
| `1.1 * 3` | 3.3000000000000003 | 3.3 |
| `0.1 * 3` | 0.30000000000000004 | 0.3 |
**近似是可见的。** 没有有限十进制形式的值在打印时会带有前导 `~`：`1 / 3` 显示为 `~0.333333333333`。它在内部仍然是精确的 —— `(1 / 3) * 3` 精确为 `1` —— 该标记仅表示*文本*是一个近似值。
**舍入是一个命名操作**，因此它会出现在派生中：
```
due = 64.92
round to 2 places = 64.92
total = 64.917525
+ = 64.917525
subtotal = 59.97
tax = 4.947525
```
**外部数字在边界处变为精确值。** 一个 JSON 的 `0.1` 从那时起就是十分之一，因此对抓取数据进行算术运算与对 literals 进行算术运算一样精确。
**代价是受限的，而非隐藏的。** 将许多具有不相关分母的分数相加会增大分母。对 2000 个不同的分数求和大约需要 10 毫秒；超过界限后，操作会被*拒绝*而不是静默舍入，因为拒绝是可见的，而舍入不是。
## Effect 表面
`shapes.py` 计算程序**能**做什么，而无需运行它。运行时 effect 日志记录了一次运行**已经做了**什么。两者必须一致，并且这种一致性作为预言机在 repo 中的每个示例程序上得到强制执行——这是唯一能够捕获不可靠分析器的检查。
升级 diff 是它存在的关键案例。它返回状态码 1 退出，因此可以用作 CI 门控：
```
$ python3 shapes_cli.py --diff demo/v1.planes demo/v2.planes
demo/v1.planes -> demo/v2.planes
NEW BOUNDARIES CROSSED: network
+ network: ask https://telemetry.example.com/collect?data=['debug', 'verbose']
+ network: ask https://telemetry.example.com/collect?data={...} (computed)
```
关于它的工作原理，有两件事值得了解。
**Effect 通过不动点算法在调用图中传播**，而不是通过遍历树，因此调用者会传递性地继承其被调用者所做的一切，并且相互递归会终止。
**一个库并不仅仅因为在加载时没有运行任何代码就是纯的。** `effects` 是运行该文件所执行的操作；`declared` 是其中任何函数如果被调用所能做的操作。包查询读取的是 `declared` —— 否则，一个唯一的网络调用深埋在某个函数内部的库会被标记为无害。
### 常量传播
Effect 目标通过变量、字符串拼接和调用参数进行解析，因此宿主保持可见，而不是坍缩成 `{...}`：
```
let base = "https://api.example.com"
let endpoint = base + "/users"
x = ask endpoint → ask https://api.example.com/users
```
放宽到未知状态总是可靠的 —— 它损失的是精度，而永远不会破坏正确性。在分支或循环内赋值的名称在汇合点处放宽，并且递归函数永远不会被特化，因为在调用 `countdown of 3` 时绑定 `n = 3` 将只会报告 `show 3` 而遗漏 2、1、0。
## 原因
出处通过 `Deriv` 节点附加在值上进行传递，而不是通过类型或签名。`apply_op` 完全不知道 derivation 的存在 —— 结果是在事后被包装的。这就是与标签传播方案在架构上的不同之处：没有任何东西会扩散到 `+` 的签名中。
```
why z → 8 from x (5) + y (3)
why result → 5 from add(2, 3) = a (2) + b (3)
why bumped → 500 from s ({record}).score + 50
```
完整的传递树，可以回溯到每个值进入程序的位置：
```
label = REQUESTS
upper of = REQUESTS
name = requests
.name = requests
info = {record}
.info = {record}
pkg = {record}
ask https://pypi.org/pypi/requests/json = {record}
<- entered at network:https://pypi.org/pypi/requests/json
```
`origins(value)` 仅返回值所依赖的边界跨越。`why` 和 `origins` 都在所有三个栈中实现，包括自举的栈。
## 规则
治理是位于 effect 表面之上的一个平面，而不是被硬塞进运行时的功能。一条规则为自身命名，指明一个主体，并禁止或允许某种 effect：
```
rule [readings-stay-local] anything may not ask to "https://metrics.internal/ingest"
```
针对计算出的表面进行静态检查，发现违规时以状态码 1 退出：
```
$ python3 shapes_cli.py demo/rules/violation.planes --rules
[readings-stay-local] violated at line 9.
ask https://metrics.internal/ingest
rule declared at line 1: anything may not ask to "https://metrics.internal/ingest"
```
规则既可以允许也可以禁止，可以指明比 `anything` 更窄的主体，并且可以通过名称和指纹相互取代 —— 因此，放宽早期规则的后续规则必须说明它是针对哪一条规则的，并且这对规则会被报告出来，而不是通过声明顺序来解决。一条永远不会触发的规则会被报告为空操作 (vacuous)，而不是静默通过。
## 标注
两种形式将人类层面的原因带入程序中，而不会改变程序的行为：
```
cap = 200 because "board policy, ratified March"
note:
from "GDPR Article 17"
derives-from [refund-cap]
```
`because` 附加到绑定上，并会呈现在 `why` 中：
```
$ python3 planes.py annotated.planes
200 from 200
because "board policy, ratified March"
refund 150 approved: true
```
**惰性是一项保证，而不是一种约定。** 从程序中剥离所有标注绝对不能改变其输出、effect 日志或其计算出的表面 —— 并且这是针对 repo 中的每个 `.planes` 文件进行断言的，而不是基于抽样。允许 `why` 的输出有所不同，因为这正是编写它的意义所在。
## 错误指明修复方法
一条报告了不匹配却没有说明应该改写什么的消息，会让其作者——无论是人类还是机器——面临一个真实的陈述却无路可走。因此，每个错误都会指明其修复方法，并且这是经过统计的，而不是断言的：
```
$ python3 errors_coverage.py
names a fix 111 of 116 (96%)
deliberately names none 5 of 116 (4%)
should name one and does not 0 of 116 (0%)
116 raise sites across interp.planes, parser.planes, lexer.planes, json.planes:
names a fix 76 of 116 (66%)
deliberately names none 40 of 116 (34%)
should name one and does not 0 of 116 (0%)
```
**两个工作列表均为零** —— 该承诺在参考实现和自举实现中都得到了遵守。
中间状态是承载负担的部分。未指明修复的代码点必须用文字在抛出点说明*原因*：parser 的通用 token 门控知道哪个 token 是预期的，但不知道作者的本意，而 `fail` 自身的消息归属于编写它的人，因此语言绝不能将其建议附加到一句并非由它编写的句子上。没有说明原因的静默状态会被视为一个缺口。
`errors_coverage.py` 仅作报告，绝不让构建失败 —— 一个诚实的行错误不应该成为无法提交的阻碍。设计记录位于 [`docs/error-messages.md`](docs/error-messages.md)。
## 模块
`use http` 和 `use file` 指明了 builtin 能力模块。`use config` 指明了一个文件 `config.planes`，它是相对于导入者进行解析的。
一个包的 effect 表面包含了它导入的所有内容的表面：
```
$ python3 shapes_cli.py demo/app/main.planes --no-follow
file:
write out.json
unresolved calls: package
```
`main.planes` 不包含任何网络代码 —— `ask` 位于 `net.planes` 中，而基础 URL 位于 `config.planes` 中。跟踪导入可以找到它，并跨所有三个文件解析出确切的 URL。如果不进行跟踪，则会如实说明，而不是报告一个它无法担保的纯净表面。
**名称在整个模块图中是扁平的，冲突即为错误。** `api base` 被调用为 `api base`，而不是 `config.api base`，因为多词名称读起来已经像散文了。扁平名称使得冲突变得真正具有歧义，因此会被报告出来：
```
module error — two modules define the same name:
'load record' is defined in cache.planes, loader.planes
try: rename one of them — names are flat across modules,
so 'load record' has to mean one thing
```
其中一个读取文件，另一个访问网络。让加载顺序来决定将意味着同一个程序会因为其 `use` 行的顺序不同而产生不同的行为，而且没有任何可供阅读的解释来说明原因。
**冲突在使用点被修复**，因为两个冲突模块的消费者通常无法编辑其中任何一个：
```
use loader
use cache with load record as load cached
fresh = load record of "requests" # loader's, over the network
old = load cached of "requests" # cache's, from a file
```
重命名*替换*了导出的名称，而不是添加别名 —— 同时注册两者将直接导致冲突再次出现。
## 外部函数
在宿主中实现的函数会声明它所做的事情。Planes 无法看到宿主内部，因此它从不猜测：
```
foreign sort of xs from "builtins.sorted" doing nothing
foreign now from "time.time" doing clock
foreign grab of u from "x.y" doing ask, clock
```
**声明的 effect 可以指明其目标**，既可以是一个固定的目的地，也可以是调用者提供的参数：
```
foreign send of x from "m.post" doing ask "https://api.example.com"
foreign fetch of url from "u.urlopen" doing ask url
```
参数形式是极具价值的：在具有已知参数的调用点，常量传播会解析出真实目的地，因此宿主名称能够跨越外部边界存活 —— 这正是让 diff 在 FFI 中具有意义的关键。
`doing` 子句是**由编写该行代码的人做出的声明**，而不是分析器推导出的事实，并且表面会如实说明：
```
ambient:
clock time.time (declared, not verified)
```
**省略 `doing` 并不意味着纯。** 它意味着未知，表面会报告这个漏洞而不是隐藏它：
```
foreign:
unknown — m.f declares no effects
this surface is incomplete: a foreign function states no effects
```
该默认设置是整个安全属性的核心。从宿主中派生 effect 在通常情况下是不可能的 —— 这将意味着需要分析 CPython，然后再分析一个 C 扩展 —— 并且失败将是静默的：一个无法看到内部的分析器会报告“纯”，从而将猜测作为事实发布。
## 宿主
Planes 运行在**宿主**上：任何实际执行 effect 的事物。一个宿主就是 **7 个方法**，这就是该语言对一台机器的全部要求。
| 方法 | 用于 |
|---|---|
| `ask` | 一次网络往返 |
| `read` | 读取文件 |
| `write` | 写入文件 |
| `show` | 输出一行 |
| `clock` | 时间 |
| `resolve` | 查找外部函数 |
| `parse_json` | 解析 JSON 文本 |
它之所以很小，是因为 effect 词汇表是封闭的：不能向宿主要求超出语言所能命名的范围。这七个方法中的每一个都有活跃的调用者 —— 这是通过机械方式检查的，因此一个停止使用的方法会变得可见，而不是成为第二个宿主不得不白白实现的死表面。
```
from host import TestHost
from interp import Interpreter
host = TestHost(responses={"https://x/y.json": '{"n": 1}'})
i = Interpreter(host=host)
i.run('use http\nr = ask "https://x/y.json"\nshow text of r.n')
```
外部目标对语言是**不透明的** —— parser 将其存储为字符串，分析器从不读取它 —— 因此 `node:fs#readFile` 和 `crate::mod::fn` 今天就能被解析和分析。更换宿主不需要更改语言，这正是 JavaScript 实现得以存在的原因。
## 机器可读表面
该语言将自身描述为数据，这些数据是从实现中生成的，而不是手工维护的，因此工具永远不必为了学习词汇表而去解析散文。
| 文件 | 包含内容 |
|---|---|
| `grammar/vocabulary.json` | 关键字、builtins、effect 类型、token 类 |
| `grammar/errors.json` | 每个错误位置：tag、类、模板、slots、fix |
| `grammar/rules.json` | parser 接受的每种规则形式 |
| `grammar/core.json` | 自举实现可以使用的子集 |
```
{
"id": "interp.cannot-compare.equal-4",
"kind": "error",
"class": "PlanesError",
"tag": "cannot-compare",
"source": "interp.py:119",
"raised_in": "equal",
"template": "records have different fields: {sorted(set(a) ^ set(b))}",
"slots": ["sorted(set(a) ^ set(b))"],
"fix": "compare records with the same fields"
}
```
如果其中任何一个偏离了它所描述的代码，`grammar_gen.py --check` 将导致构建失败。`shapes_cli.py --json` 本着相同的精神发出 effect 表面。
## 布局
这是一个方位指南，而不是一份清单。如需完整列表，请询问 repo：`git ls-files`。
| | |
|---|---|
| `lexer.py` `parser.py` `interp.py` | 参考实现 |
| `planes_num.py` `planes_text.py` | 精确有理数；作为码点的文本 |
| `shapes.py` | 静态 effect 分析器 |
| `rules.py` | 规则平面，针对表面进行检查 |
| `render.py` | 规范打印机 —— 解析、渲染、重新解析、达成一致 |
| `modules.py` `host.py` | 模块图；宿主接缝 |
| `planes.py` `shapes_cli.py` | 两个 CLI |
| `js/` | JavaScript 实现，外加 Node 和浏览器宿主 |
| `index.html` | 在浏览器中运行和分析 Planes，无需构建步骤 |
| `paint.html` | 运行 Planes 程序并将其 `show` 输出绘制到 canvas 上 |
| `grammar/*.planes` | **用 Planes 编写的 Planes** —— lexer、parser、解释器、JSON |
| `grammar/*.json` | 上述的机器可读表面 |
| `corpus/` | 规范语料库 —— 每个构造，以程序形式存在 |
| `demo/` | 用于 diff、index、规则和模块演示的小程序 |
| `identity/` | 视觉标识 —— 标记、标志组合、社交卡片，全部由 `render_logo.py` 生成 |
| `scripts/ci.sh` | 门控 |
| `docs/` | 设计记录 |
| `reports/` | 每次构建生成一份 `REPORT_*.md`，包括每次推翻了什么假设 |
## 门控
```
$ bash scripts/ci.sh
== suites: 56 files, 56 reporting, 1124 oks, 10 job(s), 45.6s wall ==
```
它运行测试套件、JavaScript 测试、锁定构造审计、语法数据检查、每个自托管文件的核心子集检查、覆盖率报告、`ruff` 和 `mypy`。`scripts/ci.sh --fast` 会跳过最慢的十二个套件以进行迭代，但它**不是**门控 —— 它跳过了跨实现的一致性检查，而这才是最值得检查的部分。
它强制执行两种习惯，这都是惨痛教训的总结：
**报告无结果的测试文件会导致构建失败。** 在这个 repo 的历史中，有五次出现了某些东西存在、通过了测试，却从未被执行的情况 —— 两个没有 runner 的套件，47 个没人运行的 JavaScript 测试，以及七个验证脚本（其中两个已经悄然出错）。警告取决于是否有人去阅读它。
**每个形似测试的文件都会被计入门控运行的内容中。** 该检查从 `ci.sh` 中读取 glob 模式，而不是重新声明它，因此两者不会悄无声息地产生偏离。
## 状态
正在运行，且已经过检查。这里没有任何内容是规范 —— 实现即是规范，而 `grammar/*.json` 是其机器可读的投影。`reports/REPORT_*.md` 文件是构建记录；每份记录的结尾都写了该构建推翻了其自身计划的哪些假设，这通常是最有用的部分。
## 许可证
[Apache License 2.0](LICENSE) — 版权所有 2026 R. Michael Thomas。
`identity/render_logo.py` 嵌入了采用 [Red Hat Display](https://github.com/google/fonts/tree/main/ofl/redhatdisplay) 字体设置的单词“Planes”的轮廓，
© 2019 Red Hat, Inc.，基于 SIL Open Font License 1.1。此处未重新分发任何字体文件。请参阅 [NOTICE](NOTICE)。
标签：云安全监控, 形式化验证, 数据可视化, 数据溯源, 编程语言, 编译原理, 逆向工具, 静态分析