你的第一个程式
今日可编译的小型端到端程式,加上规范级知识版本。
你的第一个程式
一个有意义的第一个Sounio程式应该展示这种语言的不同之处,而不仅仅是可以打印字符串。最小的当前例子,有实际身份,是一个程式,它创建一个知识值,保持这个知识包装完整,并在显式的边界处才解包。
今日稳定的
- 检查的产物仍然强制对
知识值使用显式的解包边界,而不是默默地丢弃知识上下文。 - 编译失败万古霉素固定件展示了信心约束可以参与真正的拒绝路径。
- 设计文档中描述的更丰富的确定性和证明模型比产物验证的表面更大,所以例子在这里保持在保守的子集中。
一个第一个知识程式
fn main() with IO {
let dose = Knowledge { value: 42.0 }
let accepted: f64 = dose.unwrap("demo boundary")
println(accepted)
}
如何验证它
export SOUC_BIN="$(pwd)/bin/souc"
export SOUNIO_STDLIB_PATH="$(pwd)/stdlib"
"$SOUC_BIN" check first_program.sio
"$SOUC_BIN" check tests/run-pass/vancomycin_propagation.sio
"$SOUC_BIN" check tests/compile-fail/vancomycin_low_conf.sio
这如何映射到仓库
self-hosted/check/epistemic.sio是当你想要了解当前自托管的知识检查器的工作时,要检查的实现区域。docs/reference/KNOWLEDGE_REFERENCE.md和docs/research/vancomycin-uncertainty.md解释了更大的预期模型和临床拒绝案例研究。tests/run-pass/vancomycin_propagation.sio是最小的验证位置,可以在一个真实的固定件中看到信心传播。
不要假设的
- 不要假设每个在正式知识模型中描述的字段或传播规则都由检查的产物强制执行。
- 不要假设自托管的运行时执行覆盖每个
知识密集的程式,即使check成功;一些代码生成限制仍然存在。 - 在教授Sounio时,保持当前检查的合同和更广泛规范级的设计的区别清晰。