charles0

也许可以先试试线上租 GPU ，比如 autodl, runpod ？

我也曾经想开发一个编程语言，可惜止步于一个简单的 demo ，而这个 nature 语言已经达到了相当完善的地步，实在厉害。
而且我发现 https://nature-lang.org/docs/contribute 这篇文档很不错，信息量很大，值得那些对现实中的编译器感兴趣的人阅读

补充一下，刻录的普通光盘、U 盘、固态硬盘受限于它们的特点不适合存储冷数据，磁带需要定期倒带

0. 区分热数据、备份、存档：我认为备份是可以在短时间(几天)内低成本取回的，而存档在短时间内不能取回的数据，如果要取回的话时间很长而且可能需要很多钱，同时备份需要尽可能和热数据同步并随时更新但存档不需要，而且备份可能会定期删除；这里备份和存档都是完全的冷数据，并且平常不应该尝试取回，平常你们只应该从本地硬盘/NAS/网盘之类的地方得到数据，而不是从备份处取回数据
2. 不可避免地，你需要持续投入和维护，至少一年一次对备份数据的完整校验，对于 7x24 运行的设备需要实时监控存储设备状态（ SMART 信息等等）并适当地更换和淘汰存储设备
3. 不要使用高级和复杂的技术，相反要尽量使用简单和普及的技术，因此我不建议你用光盘、蓝光光盘、磁带，我知道这些技术很好也很适合保存备份或存档，但是事情没有那么简单和理想化，你仍是个人而不是企业，你应该用大量、廉价、消费级的设备而不是少量高端、昂贵或企业级的设备，我认为 3.5 寸非叠瓦盘的机械硬盘目前最好
4. 因为你要保存几十年，所以你可能必须更新你的备份方案，假设以后机械硬盘越来越少并且主板上都不带 SATA 接口，那么你就要切换到新的技术，哪怕这种新技术不适合存储冷数据（比如 M.2 固态硬盘）
5. 云盘不可靠，可以考虑作为额外的存档，但是需要加密，唯一的问题是有些云盘会主动删除和屏蔽加密了的文件，你只有在下载的时候才会报错；对象存储只考虑 AWS S3 Glacier Deep Archive ，也是作为存档，其它的不用考虑

可以试一试 Kopia (它有图形界面版本 KopiaUI) + rclone 的方案

连 GPT-4 都能回答正确，它第一句话就是：在讨论 uv, yarn, npm, 和 pnpm 之间的区别之前，我想先澄清一下可能存在的误解。uv 在这个上下文中可能是一个笔误，因为 uv 通常不与包管理工具相关联。假设你指的是 npm, yarn, 和 pnpm 这三种 JavaScript 包管理工具，我将基于这个假设来进行比较。

但是它的回答的第一行还是有一点迷惑性，虽然后面具体解释 uv 的时候它说 uv 可能是指 Deno 的 uv 库：在某些文档中提到的 uv 可能指的是 Deno （一个新的 JavaScript/TypeScript 运行时）所用的底层库 libuv ，这是一个提供事件驱动、异步 I/O 操作的库。它不是一个包管理工具，而是用于 Deno 环境中的底层 I/O 操作，类似于 Node.js 中的 libuv 库。

gpt-4.5 指出：uv 不是一个包管理工具，更多是指与 Deno 相关的底层库（如果你是指这个）。
https://chat01.ai/zh/chat/01JQ84ZZVPWVW58EEX8C5QSZXT

我设想中的编程语言不仅要强类型+静态类型，还要有一定的形式化验证能力和依赖类型，像 Dafny 语言、Idris 语言和 Ada/SPARK 语言那样尽可能静态地保证程序的正确性，让 AI 在编写代码的同时还编写证明。目前看来经过合适的训练以后 AI 可以编写证明过程，参考 DeepMind 的 AlphaGeometry 项目解决的几何证明题。现有的形式化验证项目如 seL4 和 CompCert 最大的问题是一行普通代码可能对应十几行证明，开发效率太低，如果能用 AI 的话可能可以大大加快对关键基础设施开源项目的形式化验证。目前我想到的最大问题还是语料不足和 AI 成本比较高。