主要观点：TLA⁺由 Leslie Lamport 开发，其语法类似 LaTeX，有很多数学符号。文中介绍了作者将 TLA⁺中的美丽符号引入代码编辑器的过程，包括构建 Unicode 工具链，如 TLA⁺树状语法、ASCII/Unicode 转换工具、Neovim 插件等，并在多个项目中使用。之后作者决定在 TLA⁺主要语言工具中实现 Unicode 支持，面临技术难题如代码测试覆盖率低、代码生成和修改导致的死锁等，通过编写大量测试解决。在 FOSS 合作中，作者体会到与在公司开发的不同，学会用 git 提交作为沟通工具，总结出良好的 FOSS 贡献行为要点。最终 添加 Unicode 支持到 SANY 的最终 PR 被合并，为未来语言发展打开可能，作者也面临 FOSS 资金问题。
关键信息：

• TLA⁺语法含多种数学符号，有tla2tex命令将其格式化为 LaTeX 用于研究论文。
• 作者构建了个人 Unicode TLA⁺工具链并在多个项目中使用。
• 在 TLA⁺主要语言工具中实现 Unicode 支持面临技术难题及解决办法。
• FOSS 合作与公司开发的不同及学会的沟通方式。
• 最终 Unicode 支持的 PR 被合并及未来展望。
  重要细节：
• 文中提到不同相关语言对 Unicode 的支持情况，如 APL 早在 60 年代就有相关要求，Lean 和 Agda 显示将 Unicode 符号融入对终端用户较方便，而 Idris 目前不支持。
• 介绍了 TLA⁺主要语言工具的代码情况，如大量 25 年历史的 Java 代码、静态全局变量、测试覆盖率不一等。
• 阐述了在 FOSS 中接受贡献的门槛高于公司，以及用 git 提交作为沟通工具的要点。
• 提到 TLA⁺基金会及相关工作资助方式。