主要观点：

• Bertrand Meyer 和 Reto Weber 的“Meaning as Programs”及“Programming Really Is Simple Mathematics”预印本，2025 年 2 月发布，可在此处[https://se.inf.ethz.ch/~meyer...]和 arXiv[https://arxiv.org/abs/2502.17149]获取。
• 编程理论可很复杂，此呈现回归本质，仅用初等集合论概念定义编程及相关概念，如编程语言、编程方法学。
• 名为 PRISM 的方法公理少定理多，基于一个集合和一个关系，借助集合论性质构建编程机制并证明定理。
• 该方法始于 2015 年文章，如今得益于 Reto Weber 在 CIT 的工作，有大量经 Isabelle/HOL 检查的证明，相关文件可公开获取。
• 文章涵盖一般框架，包括数学背景（高中水平初等集合论及相关便利符号）、基本构造、控制结构、细化、规范与实现、合同、不变量和并发等。
• 旨在以这种精神重建所有编程，论文抽象强调零公理、单个概念涵盖规范和程序等。
• 所有定理都经机械验证（用 Isabelle/HOL），证明可在公共仓库获取。

关键信息：

• 2025 年 2 月有相关预印本发布及获取途径。
• 编程理论回归本质用集合论定义相关内容。
• PRISM 方法特点及始于 2015 年。
• 涵盖多方面编程内容及相关证明。

重要细节：

• 提及 Reto Weber 是 CIT 的博士生。
• 说明定理经 Isabelle/HOL 验证及证明可获取。
• 给出作者完整注释出版物列表地址。
• 有投票评级相关信息。