13 篇文档带有标签「Research」

基于 idea/ 中的项目选择判据与手工艺讨论，延伸讨论广义代码正确性在 AI 时代的变化——以数值计算为具体抓手，但不限于此。

承接 [[AI时代数值代码的正确性来源.md]] 的讨论——该文论证了在 AI 时代，正确性工程的投资重点应从"怎么写得对"转向"怎么知道它是对的"，判断型资产比代码型资产更值钱。

承接 [[AI时代数值计算编程语言选择.md]]——那篇讨论了"直接使用现有语言，怎么选"。本篇讨论一个不同的问题：

调研时间范围：2025–2026 年 | 涵盖 Web / Mobile / Desktop GUI / 游戏四大方向

关联文档：[[项目诊断.md|项目诊断]] 中的语言选择部分推荐了 Rust 作为"最值得新学的语言"——但 Rust 的科学计算生态到底多成熟？ChemE/PSE 相关的库够不够用？

承接 [[AI时代数值计算编程语言选择.md]] 和 [[AI时代数值计算语言改造基础选择.md]] 的讨论——在讨论了"AI 时代怎么选数值计算语言"和"哪个语言基底最适合被改造"之后，本文聚焦一个具体问题：

A comprehensive timeline across operating systems, programming languages, and numerical computing software.

摘要

梳理 Why3 支持的所有后端证明器，评估其浮点数约束与常用数学函数（sin/cos/exp/log 等）的支持能力。可作为 [[数值函数形式化验证-中间语言与验证平台选型.md]] 和 [[数值函数形式化验证-想法与约束.md]] 的补充参考。

基于 [[数值函数形式化验证-想法与约束.md]] 中 PureLibm-rs 五级验证体系，探索 Rust 之外的验证平台选择，评估中间语言作为"一次证明、多语言分发"中枢的可行性。

综合自 idea/ 中的多份讨论：[[PureLibm-rs.md]] 的项目设计、[[项目诊断.md]] 的项目 B 评估与手工艺候选分析、[[Rust科学计算生态调研.md]] 的 LLVM/浮点约束章节、[[项目选择判据-双视角.md]] 的判据框架、[[个人项目选择规则.md]] 的数学库规则。

摘要

问题场景