Linux 基金会成立 TLA+ 语言基金会

Linux 基金会宣布成立 TLA+ 基金会 (TLAF)，以促进 TLA+ 编程语言及其 TLA+ 从业者社区的采用和发展。TLA+ 基金会的创始成员包括 AWS、甲骨文和微软。

TLA+ (Temporal Logic of Actions) 是一种用于对程序和系统 (尤其是并发和分布式程序和系统) 进行建模的高级语言。Linux 基金会表示，TLA+ 语言已被成功用于验证复杂的软件系统、减少错误并提高可靠性；其有助于在开发过程的早期发现设计缺陷，节省时间和资源。“TLA+ Foundation 的成立旨在推动采用经过验证的形式化方法来构建稳健的软件。”

该语言在几十年前由现任 Microsoft Research 杰出科学家 Leslie Lamport 发明，基于“精确描述事物的最佳方式是使用简单的数学”的理念。时至今日，其管辖权逐渐从微软转移到 Linux 基金会，并获得了自己独立的基金会来推广发展。

根据介绍，TLA+ 基金会是一个独立的非营利组织，致力于促进 TLA+ 规范语言在工业界、学术界和教育界的采用，其总体目标是推进软件工程中的数学思维。TLAF 资助与 TLA+ 相关的开发，以扩大其用途并促进繁荣的 TLA+ 社区，鼓励该社区成员之间的合作。

TLA+ 基金会将促进采用、提供教育和培训资源、资助研究、开发工具并建立 TLA+ 从业者社区。TLA+ 基金会作为语言委员会的角色将确保 TLA+ 语言的不断完善和演进。TLA+ 基金会将就语言增强做出决策，解决用户反馈和需求，保持高安全性和可靠性标准，并引导语言的发展以更好地服务于其用户群。

基金会的行为准则包括：开源，全心全意地拥抱开源精神；赋予社区权力，最大限度地为 TLA+ 用户带来利益；透明性，所有正式的决策都将公开；以及秉承开放、友好、多元的精神。

Linux 基金会执行董事 Jim Zemlin 称：“TLA+ 基金会的成立表明了我们致力于推进 TLA+ 语言的使用和开发，以造福整个软件行业。随着世界对分布式系统的依赖程度不断提高，对于开发人员来说，拥有 TLA+ 的功能来正式建模和验证系统的行为是否符合预期非常重要。”