Ferrous Systems 捐赠 FLS 给 Rust 项目

Rust 自 2015 年 5 月发布 1.0 版本后，凭借速度、安全性以及活跃的社区，成为发展迅速且深受开发者喜爱的语言。然而，与其他语言相比，Rust 一直缺少一份官方语言规范。

1. 规范缺失与推动：2022 年 12 月，一份鼓励 Rust 项目着手制定规范的 RFC 提交，经过讨论，于 2023 年 7 月获批并启动相关工作。
2. FLS 的诞生：2022 年 7 月，Ferrous Systems 为用于安全关键和受监管行业的 Rust 编译器及工具链 Ferrocene 开发了 Ferrocene 语言规范（FLS），它对 Rust 的语法、语义和行为进行了结构化、详细的描述，为验证、合规和标准化工作提供了基础。
3. 捐赠与整合：Rust 项目规范团队（t-spec）为避免行业内出现两份规范造成混淆，决定尝试将 FLS 与 Rust Reference 整合以创建官方规范。Ferrous Systems 同意将 FLS 捐赠给 Rust 项目，并由 Rust 项目接管其开发和管理。
4. 意义与影响：此次捐赠为 Rust 项目制定官方规范提供了更清晰的路径，增强了依赖 FLS 的公司和个人的信心，标志着 Rust 生态系统的一个重要里程碑。未来，FLS 和 Rust Reference 将共同构成官方的 Rust 规范。

原文：https://rustfoundation.org/media/ferrous-systems-donates-ferrocene-language-specification-to-rust-project/

使用 MASH 技术栈快速构建 Web 项目

作者在开发个性化内容推送网站 Scour 时，采用MASH 栈（由 Maud、Axum、SQLx 和 HTMX 组成）。Maud用于编写类型安全的 HTML 模板；Axum是 Web 框架，能解析 HTTP 请求；SQLx处理数据库操作；HTMX增强网站交互性且其 JS 可缓存。该栈虽有编译时间长、加载静态 HTML 片段不够优雅等不足，但各组件协同性好，适合用 Rust 开发网站的人尝试 。

选择 MASH 栈的原因：在评估多种框架和库后，作者确定了这几个关键组件，且发现其被称为 “mash stack”。Scour 采用服务器端渲染 HTML，因为浏览器渲染 HTML 速度快，且网站无需过多复杂交互，遵循 “YAGNI” 原则。其中：

• Maud：编写 HTML 模板。在 Rust 代码中编写，格式简洁、类型安全，支持控制结构和部分模板复用
• Axum：Web 框架。使用函数和提取器解析 HTTP 请求
• SQLx：数据库操作库。支持 SQLite、Postgres 和 MySQL，可通过派生 FromRow 映射数据库行和 Rust 类型
• HTMX：增强网站交互性。通过 HTML 属性控制 HTTP 请求和响应，避免直接写自定义 JS，其 JS 可缓存

MASH 栈的协同作用

• 页面布局提取器：Axum 的提取器可实现页面布局复用，Maud 的Markup可直接从 Axum 路由返回。
• 缓存预加载请求的中间件：HTMX 的预加载扩展与设置缓存响应头的中间件配合，提升用户体验。

使用 MASH 栈的不足

• 编译时间：Rust 开发普遍存在编译时间长的问题，开发过程中通过工具和优化可将保存到页面重新加载时间缩短至约 2.5 秒。
• 加载静态 HTML 片段：HTMX 通过后端交换 HTML 块实现交互有时较笨拙，可结合其他技术改进。

原文：https://emschwartz.me/building-a-fast-website-with-the-mash-stack-in-rust/

Kani: Rust 模型检查器

Kani 是一个用于 Rust 的精确模型检查器，特别适用于验证 Rust 中的不安全代码块。以下是该仓库的详细介绍：

• 内存安全（例如，空指针解引用）
• 用户指定的断言（即 assert!(...)）
• 无 panic 情况（例如，在 None 值上调用 unwrap()）
• 无某些类型的意外行为（例如，算术溢出）

类似于编写测试，用户需要编写一个验证 harness，但使用 Kani 可以通过 kani::any() 检查所有可能的值。示例代码如下：

use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input = kani::any();

   // Constrain it according to the function's precondition
   kani::assume(precondition(input));

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}

Kani 会尝试证明所有有效的输入都能产生可接受的输出，且不会发生 panic 或执行意外行为。如果验证失败，Kani 会生成一个指向失败点的跟踪信息。

Github 仓库：https://github.com/model-checking/kani

--

From 日报小组 Yuan YQ

社区学习交流平台订阅：

• Rustcc 论坛: 支持 RSS
• 微信公众号：Rust语言中文社区