最新

SunCalc 是我最早的开源项目之一——15 年前我提交了第一个版本，此后它得到了广泛的应用，但近年来却有些被忽视了。现在，现代人工智能工具使我能够解决多年积累的技术债务和用户问题，我终于有能力复兴像这样的项目并保持它们的良好状态。 v2 是一个新版本，将太阳的计算精度提高了 5 倍，月亮的计算精度提高了 20 倍，并通过一个广泛的测试套件与美国海军天文台的地面实况进行了验证，此外还修复了大量问题，并使用 ESM 对分发进行了现代化改造。希望您喜欢。

<a href="https://www.macrumors.com/2026/06/18/a12-and-a13-chips-facing-exploit/" rel="nofollow">https://www.macrumors.com/2026/06/18/a12-and-a13-chips-facin...</a>

我一直在尝试将不同类型的谜题融合在一起，并重新发明了我称之为“数独单词搜索”的东西。这是一种字母数独谜题，其中单词隐藏在谜题中，你需要推断出单词的位置才能解开谜题。 也就是说，仅凭数独逻辑无法唯一地解开这个谜题。你必须使用两种隐藏单词的逻辑之一来完成谜题：1）推断出单词必须放置的位置并添加字母，或者 2）推断出单词不能放置的位置并限制字母。为了使其更像数独并帮助解题，每一行、每一列和每一个九宫格都至少包含一个已找到单词的字母。 在游戏测试中，我觉得它很有趣，尽管有时对我来说非常困难（我不是数独专家），所以我想把它开发出来分享。 谜题的生成过程是这样的：创建包含 9 个独特字母的字母组，找出所有可以用这些字母组成的单词，生成示例网格，在其中找出单词，剔除不符合单词放置标准的候选谜题，然后通过删除字母来“雕刻”棋盘，直到满足两个条件：数独逻辑的解题方案大于等于 2 个，并且加入单词搜索逻辑后只有 1 个解题方案。总的来说，大约会生成并剔除 60000 个谜题才能得到一个有效的谜题。 我在代码编写过程中广泛使用了 Claude，其中包括： - 谜题生成器 - 谜题解算器 - 谜题解释器 - 静态网站 (Cloudflare) - 在线谜题播放器 (本地存储) - 在线静态谜题 walkthrough - 打印书籍布局 - PDF 布局 总的来说，花几周时间专注于此让我感到非常有趣。 https://www.sudokuwordsearch.com

我认为在像旧手机这样的设备上搭建一个论坛会很有用。目前是否有可用的资源或类似的项目？

您对此有什么经验法则吗？您团队中有人负责这个决定，还是由编写发布版本的人来做决定？

在 Cajal (YC W26)，我们很高兴推出 Talos（[https://github.com/cajal-technologies/talos](https://github.com/cajal-technologies/talos)），这是一个用于在 Lean 中对 WebAssembly 模块进行形式化验证的开源框架。 人工智能现在正在编写大量用于生产的代码。随着代码生成成本的降低，验证成为了瓶颈。我们相信，未来每一段软件都将附带一个数学证明，证明它实现了作者的意图——从而消除许多类型的漏洞。Talos 是实现这一目标的基础之一。 Talos 提供了一个针对二进制级别推理优化的 Wasm 解释器，以及一个用于证明程序属性的最弱前置条件演算层。由于我们直接对 WebAssembly 进行推理，因此任何具有 Wasm 后端的语言都在支持范围内：Rust、C++、Go、C、Swift、Kotlin、Zig、C# 等等。 为了实现这一点，我们使用了 Lean：一种编程语言和定理证明器，它允许您在一个系统中同时编写软件并对其进行数学证明。这使得 Talos 既可以作为可执行解释器，也可以作为 Lean 进行推理的形式化对象。Lean 还集成了现代人工智能证明工具，通过证明搜索和直接评估自动处理目标。 要查看 Talos 的实际应用，请查看对流行的 Rust crate num-integer 中实现的 Stein 的 GCD 算法的证明：[https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588](https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588)。 我们的路线图： - 通过首先通过官方 W3C 测试套件，然后对 SpecTec（形式化 Wasm 规范）进行验证，实现完整的 Wasm 覆盖。 - 任意 crate 验证——任何编译到 Wasm 的 Rust crate 都应在支持范围内。 - 构建我们的证明库 codelib，以使验证日益复杂的程序变得可行。 我们非常希望听到社区对 Talos 的反馈以及对当前形式化验证状态的评论。也欢迎贡献！