最新

大家好。在过去的两年里，我作为开发者，利用闲暇时间不断拓展我的知识边界。虽然我并不是数学家，但我发现用数学语言形式化概念对提升对这些概念的符号推理能力是有帮助的。我使用了书籍和人工智能，并且主要以批判的眼光关注后者的发展。我有几个开放的项目，从其中一个的观察和探索中，我开始思考当前推理、逻辑和数学本身的极限。因此，我探索了范畴和拓扑，尤其是从马佐拉的音乐理论出发。我思考这是否会影响编程中的类型理论，并进行了若干实验。由此诞生了这个编程语言——Yon，灵感来源于Yoneda引理和态射。另一个项目让我对Leech格进行了观察；还有一个项目则进行了关于mmap和基于坐标的分配的实验，这在拓扑意义上也是有利的。 这个语言确实存在一些错误，我匆忙编写了文档；整个工作花费了三周时间。出于性能考虑，它编译为LLVM，目前我选择避免使用虚拟机和垃圾回收。它包含一些不寻常的数据结构，结果表现出色。值得一看，我希望它能吸引一些信徒，并且有人愿意帮助我进行开发。我希望它能为编程带来新的刺激，或许还能开辟一些新领域。 对于那些想深入了解的人，这里有一些具体细节。编译器是一个真正的流水线，而不是解释器：一个OCaml前端将.yon源代码转换为我称之为“topos”的自定义MLIR方言，其中范畴构造作为一等公民存在；它的降级过程将所有内容转换为LLVM IR，然后生成本地可执行文件。一个命令yonc驱动整个链条，你可以在任何中间阶段停止，查看一个范畴构造在转化为硅的过程中实际变成了什么。 运行时是Leech格观察的最终归宿。堆是基于Λ₂₄的内容寻址：每个值映射到一个格点，并在康威群Co₀下进行规范化（通过libmmgroup），因此相同的内容总是位于相同的地址。这带来了三件我现在很难放弃的事情：无论值多大，等价性都是一次机器比较（字符串相等的基准测试在~17纳秒平稳运行，支持高达32,768个字符的字符串，因为它比较的是句柄，而不是字节）；去重是全局和自动的，用户代码中没有内部逻辑；放弃垃圾回收不再是一种放弃，因为单元是不可变的和内容寻址的，因此没有需要追踪和移动的内容。 我故意将并发保持得简单明了：没有线程，没有共享可变状态。程序分裂成独立的“空间”（隔离的进程，由MMU强制隔离），通过具有明确失败语义的共享内存通道进行通信。 关于验证的内容和仅仅是希望的内容：基本真相是一个包含112个示例的回归测试套件，以及一个跨空间场景套件，Linux x86-64和macOS Apple Silicon上的退出代码完全相同（Intel Mac：未测试）。网站上的书籍包含21章及附录，每个代码片段在写下之前都已编译并运行。基准测试附录声明了其环境和方法；我尽量不发布任何没有说明的数字。1.0的限制也被记录在案，作为基线文档列出了每个固定池（每条链256个堆、64个空间、16个并发RPC会话等），其理由是，响亮失败的硬限制是规范，而默默降级的软限制是一个错误。 关于许可证，我选择了GCC模型：编译器和工具链为AGPLv3，运行时为AGPLv3，附带明确的链接例外，因此语言本身保持自由，而你用它编写的程序完全属于你，可以选择任何许可证。 网站 + 书籍： [https://yon-lang.org](https://yon-lang.org) 代码库： [https://github.com/yon-language/yon](https://github.com/yon-language/yon)（标签v1.0.0） 欢迎提出任何问题：topos方言、为什么选择格而不是哈希、范畴构造降级到什么、在这个过程中遇到了什么问题。

市场营销工程师为市场营销人员服务，设计工程师为设计师服务，卫生工程师为清洁工服务——按照这个逻辑，收银工程师应该是下一个为结账时为你服务的人而设的职位。 这种头衔膨胀是怎么回事？为什么仅仅因为你编写软件就要称自己为工程师？在我看来，工程师是那些构建事物并对其承担全部责任的人——设计一座桥梁，数千条生命掌握在你手中，制造飞机引擎，过滤城市的水源。这不是在机器上按键。