🔥 今日焦点

周一的头条是 Karpathy 给「pelican on a bicycle」这个经典 AI 图像基准判了毕业（375 分，今日 HN 最高）——他暗示这个 2024 年由 Simon Willison 带火的测试已经被模型攻克，评论区立刻分裂：一方认为模型画的 pelican 还在犯「两条腿在自行车同侧、长两只喙」的低级错误，说解决纯属自欺；另一方认为争论已经退化到「哪只 pelican 更好看」的品味层面，这本身就是模型不再明显失败的拐点证据。两条线其实都成立——基准的区分度确实枯竭了，但把它说成「已解决」是另一回事。第二条线更有意思：Lean 定理证明器内核的 soundness bug #14576，是被一个 LLM「证伪」Collatz 猜想的事件牵出来的——LLM 声称证明了 Collatz 猜想有反例，结果反例本身是证明器内核漏洞的产物。形式化验证号称能终结「AI 幻觉」，结果验证器自己的信任链先断了。第三条线是怀旧系大爆发：NetBSD 11.0 正式发布（Lobsters 99 分居首）、RISC OS Open 二十周年、6502 上跑自回归语言模型、CP/M-386 复活——老平台在 AI 时代反而成了避风港。

🤖 AI 与模型

  • Karpathy 的 Pelican — Karpathy’s Pelican。375 分 / 296 评论（HN）。今日最高分帖：Karpathy 暗示「pelican on a bicycle」基准已被攻克。💬 Morromist 直接开火——AI 画的 pelican 至今还有两条腿在自行车同侧、甚至长两只喙，「换个测试」不等于「通过测试」；jonas21 反驳说争论已进入「哪只更好看」的品味之争，这本身就是模型不再以明显方式失败的信号。
  • 我的个人 AI 基准：生成一只哈布斯堡下巴的青蛙 SVG — My personal AI benchmark: “Generate an SVG of a frog with a Habsburg jaw.”。76 分 / 42 评论（HN）。个人基准的极致形态——要求模型画出「哈布斯堡王朝标志性下巴」的青蛙 SVG，考验的是 SVG 编码能力和冷门历史知识的结合，比任何 benchmark 套件都有个性。
  • 6502 处理器上的自回归语言模型 — Autoregressive Language Model on the 6502 Processor。14 分 / 讨论中（HN）。BitNet 量化思路下放到 8 位 CPU——6502 跑自回归模型，性能不重要，「跑得动」本身就是硬核浪漫。
  • 我（基本上）按速度选模型，而不是智能 — I’m (mostly) picking models on speed now, not intelligence。△16 / 9 评论（Lobsters）。观点文章：模型智能差距对日常任务已经无关紧要，延迟才是体验分水岭——和 Karpathy 的 pelican 帖形成呼应，评测标准正在从「会不会」转向「多快」。
  • 没有数学家的数学 — Mathematics Without Mathematicians。△10 / 8 评论（Lobsters）。LLM 时代「数学不需要数学家」的命题拆解——AI 能加速计算和验证，但提出问题的能力仍然是人的活。
  • 通过手动重打 LLM 生成的代码来防止认知负债 — Prevent cognitive debt by manually retyping LLM-generated code。△25 / 12 评论（Lobsters）。反主流建议：把 LLM 生成的代码手动敲一遍再提交，用肌肉记忆换理解——评论区一半人觉得是行为艺术，一半人承认确实有效。
  • OpenAI：数学与理论计算机科学的十个进展 — Ten advances in mathematics and theoretical computer science。△13 / 1 评论（Lobsters）。OpenAI 盘点自家模型在数学上的进展——和 Lean soundness bug 帖同一天出现，时机微妙。
  • 23 种语言，只有一种我能检查 — 23 languages, one I can check。△1 / 2 评论（Lobsters）。用 LLM 写了 23 种语言的项目，作者只会检查其中一种——vibe coding 时代的自我认知问题。

🛠️ 工具与开发者体验

  • Meshdiff：浏览器端客户端对比两个 STL 版本 — Meshdiff – visually compare two STL versions in the browser, client-side。170 分 / 17 评论（HN）。3D 打印文件的可视化 diff 工具，纯客户端运行。💬 评论区共识明确：三视口缺同步旋转、希望集成进 GitHub PR 做 3D 文件审查、想要 CLI 版本进 CI——作者 roadmap 上都有，需求端已经替他把优先级排好了。
  • Show HN: MicroCodex – 用 C++ 重写 OpenAI/codex，二进制小于 1MB — Show HN: MicroCodex Coding Agent。11 分 / 3 评论（HN）。1MB 以内的 coding agent——和动辄几百 MB 的 Electron 全家桶形成对比，至少在「轻」这个维度赢了。
  • 把 Go 的 defer 加进 TypeScript 编译器 — Adding Go’s Defer to the TypeScript Compiler。13 分 / 4 评论（HN )。给 TS 编译器加 defer 关键字的实验——编译原理入门级但写得很清楚，改编译器比写业务代码好玩多了。
  • C 语言用 SDL2 重写的 Fasttracker II 克隆 — Fasttracker II clone in C using SDL 2。108 分 / 36 评论（HN）。经典 tracker 音乐软件的开源复刻，评论区全是「我的青春回来了」。
  • FlickBoard — FlickBoard。△11 / 2 评论（Lobsters）。Android 上的 flick 输入法——滑动输入的老派交互在触屏时代复活。
  • write 时遇到 EPIPE 可能说明你做错了 — EPIPE on write might mean you’re doing it wrong。△18 / 4 评论（Lobsters）。rachelbythebay 的经典论调：EPIPE 不是随机故障，是你对管道的生命周期判断错了——Unix 语义教育帖。
  • Fixi 计划 — The Fixi Project。△24 / 讨论中（Lobsters）。Lobsters 上的新项目，标签挂 practices——社区还在持续发明新的工程实践载体。
  • 笔记与个人知识管理 — Note-Taking and Personal Knowledge Management。94 分 / 26 评论（HN）。PKM 的元讨论——为什么笔记系统总是建好就弃，26 条评论里有几条说得比原文透彻。
  • 开发者依恋工具，因为工具编码了信任 — Developers are attached to tools because tools encode trust。118 分 / 58 评论（HN）。Stack Overflow 博客谈工具忠诚度——58 条评论的共识是：换工具的成本从来不是学习曲线，是「这工具值得信任吗」的重新评估。

🔒 安全与隐私

  • TP-Link TL-841N 的 root 权限、固件分析和重置后依然存在的硬编码凭据 — Rooting, firmware analysis and persistent credentials of TP-Link TL-841N。74 分 / 14 评论（HN）+ △6 / 1 评论（Lobsters）。老路由器固件逆向：硬编码凭据连恢复出厂设置都清不掉——廉价 IoT 设备的安全债，卖一台算一台。
  • SSH 凭据收割：我的蜜罐网络观察 — Harvesting SSH Credentials: Insights from My Honeypot Network。32 分 / 24 评论（HN）。蜜罐数据报告：互联网上每分钟都在发生的 SSH 爆破，凭据质量比想象中高——评论区照例提醒「fail2ban 只是安慰剂」。
  • 欧盟年龄验证项目强制硬件绑定认证 — EU Age Verification Project Mandates Hardware-Bound Attestation。85 分 / 35 评论（HN）。欧盟年龄验证方案要求硬件级 attestation——浏览器和设备厂商被迫当「年龄警察」，评论区在吵「硬件 attestation 最后会变成设备指纹监控」。
  • 加州人的数据删除请求 DROP 从 8 月 1 日起可执行 — Californians’ data deletion requests, DROP, become enforceable Aug. 1。26 分 / 1 评论（HN）。加州「删除权请求」进入可执行阶段——法规落地只是开始，真正的问题是企业有没有能力找到并删掉你的所有数据。
  • 「搞死这个女人」：eBay 骚扰行动如何导致 5600 万美元和解 — ‘Crush this lady’: how eBay harassment campaign led to $56M payout。137 分 / 60 评论（HN）。FT 长文复盘 eBay 高管策划的骚扰案——从社交媒体上的活蛆快递到威胁信，科技公司高管的判断力能低到什么程度，60 条评论全是「这居然是真的」。

💻 系统与平台

  • NetBSD 11.0 发布 — NetBSD 11.0 released。△99 / 18 评论（Lobsters）。Lobsters 今日最高分。💬 评论区亮点：官方坦言「vulnpocalypse」——AI 工具让漏洞报告激增，与其无限期推迟发布，不如带着 open issues 透明发布；新增 RISC-V 架构支持，riscv64 已有 2 万+ pkgsrc 包；有用户因为 Linus 对 LLM 的评论从 Linux 切到 NetBSD 当主力机，还有人为它专门买了 RISC-V 开发板。
  • RISC OS Open 二十周年 — Twenty Years of RISC OS Open。143 分 / 27 评论（HN）+ △5 / 0 评论（Lobsters）。Acorn 时代的操作系统开源 20 年。💬 老开发 nickcw 回忆自己的 !Director 应用全用 ARM 汇编写成；有人指出乐谱软件 Sibelius 就诞生于 RISC OS——比多数人以为的「博物馆项目」活得久得多。
  • Show HN: Kakehashi – 在 Linux ARM 上跑 macOS 二进制的实验性用户态 — Show HN: Kakehashi – Experimental userspace to run macOS binaries on Linux ARM。152 分 / 35 评论（HN）。macOS 版「Wine」：用户态直接跑 Mach-O 二进制。💬 作者 vlad_kalinkin 亲自回复：7-Zip 已跑通（比原生慢 5.2 倍，已有优化路线图）、curl 200+ 命令通过自动化测试、Xcode Git 基础命令可用；长期目标是完整 Xcode Tools（含 iOS 构建）和 macOS 版 Homebrew。评论区拿它和 Darling 对比，作者明确声明「非派生」。
  • Show HN: NixOS-DGX-Spark – 在 DGX Spark 上跑 NixOS — Show HN: NixOS-DGX-Spark。81 分 / 22 评论（HN）。NVIDIA 的 DGX Spark 个人 AI 工作站跑 NixOS——声明式系统接管 AI 硬件的尝试，评论区在讨论 CUDA 闭源驱动和 Nix 的兼容性摩擦。
  • 从 Arch Linux 辞职 — Resigning from Arch Linux。△44 / 4 评论（Lobsters）。Foxboron（Arch 安全团队核心、sbctl 作者）宣布退出——和昨天 Arch 停用 AUR 包采纳机制放在一起，治理压力的两面。💬 novedeo 说「对 Arch 安全团队和 AUR 维护者来说，这几个月的压力肉眼可见」。
  • 跨主机共享 X11 Server：FamilyWild — Sharing an X11 Server Across Hosts with FamilyWild。23 分 / 5 评论（HN）。把 X11 server 共享给多台主机用——X 协议在 Wayland 时代依然能整出花活。
  • MkLinux 和爆改版 Apple Workgroup Server 9150 — MkLinux and the pimped-out Apple Workgroup Server 9150。△12 / 3 评论（Lobsters）。90 年代 Apple 官方 Linux 移植项目的怀旧考古——oldvcr.blogspot 出品，图片质量一贯的高。
  • CP/M-386：从 CP/M-68K 派生、面向 386 保护模式的 CP/M — CP/M-386: CP/M for 386 protected mode, derived from CP/M-68K。△2 / 讨论中（Lobsters )。CP/M 移植到 386 保护模式的考古项目——和 6502 跑 LLM 同一天出现，复古计算的两极。
  • 你的计算器能跑 Linux 吗？ — But can your calculator run Linux?。△27 / 2 评论（Lobsters）。raymii 折腾图形计算器跑 Linux——「能不能跑 Linux」已经成了硬件的通用度量衡。
  • 能用树莓派做一个 Wii U 手柄吗？ — Can you make a Wii U gamepad from a Raspberry Pi?。△2 / 讨论中（Lobsters）。硬件黑客视频——Wii U GamePad 的屏幕流协议被逆向后，树莓派成了廉价替代品。

💬 编程语言

  • F*：通用、面向证明的编程语言 — F*: A general-purpose proof-oriented programming language。139 分 / 61 评论（HN）。微软研究院的依赖类型语言上首页。💬 最高赞评论是抱怨：官网翻五页找不到一个代码示例——「新语言我想要两样东西：语法长什么样、为什么要用它」，形式化验证语言的市场化问题比技术问题更迫切。
  • Lean 内核健全性 Bug #14576 事后分析 — Postmortem for Lean Kernel Soundness Bug #14576。△48 / 3 评论（Lobsters）。Leo de Moura 亲自写的事后分析。💬 背景比 bug 本身更炸：这个漏洞是被一个 LLM「证伪」Collatz 猜想牵出来的——LLM 声称找到了反例，反例其实是内核漏洞的产物；作者事先知道 bug 存在，但拒绝回答证明是否针对 bug 构造；漏洞同时命中主内核实现和独立验证器，独立性假设被击穿。
  • sizeof 在 C 里出奇地难解析 — sizeof is surprisingly difficult to parse in c。△45 / 31 评论（Lobsters）。sizeof 的类型/表达式二义性让所有 C 解析器头疼。💬 david_chisnall 给出历史答案：C 没有形式文法起步，语法就是「编译器接受什么算什么」，C89 标准化时被迫定义解析规则来兼容已有代码，早期编译器内存受限又催生了一堆省状态的解析 hack——今天的复杂度是 70 年代硬件约束的遗产。
  • OCaml 的 guard 方法 — Guarded methods in OCaml。△11 / 1 评论（Lobsters）。OCaml 类型系统里表达 guard 模式的语言设计笔记——函数式社区的日常内卷。
  • Rust 参数解析的新旧之争 — An old-new take on argument parsing in Rust。△28 / 7 评论（Lobsters）。jmmv 主张回到 getopt 式老派设计，挑战 clap 一家独大的现状——和昨天的 rand fork 帖一脉相承，Rust 生态开始出现「官方库太大」的反叛。
  • C++26 的 std::hive 有多快？ — How fast is C++26’s std::hive?。△9 / 3 评论（Lobsters）。Daniel Lemire 实测新容器——缓存不友好的场景下 hive 的优势有多大，数据说话。
  • 用 Rust 新 API 做更快的浮点运算 — Faster floating point math with Rust’s new API。△6 / 4 评论（Lobsters )。Rust 新浮点 API 的实测——性能敏感场景的微优化指南。
  • Atom 在关键方面优于 RSS — Atom is better than RSS, in ways that matter。△64 / 53 评论（Lobsters）。Lobsters 上的格式战争。💬 emk（当年和 Dave Winer 合作过 RSS 的人）长文回顾：RSS 1.0 的 RDF 化把简单格式复杂到没人能正确实现，Shirky 当年的预言全部应验；「把 Atom 改名为 RSS 3」的提议被泼冷水——RSS 3 这个名字已经被占，而且 Winer 阵营会为了商标权大打出手。

📚 轻度与好玩

  • 折叠纸地球仪 — Folding Paper Globes。134 分 / 28 评论（HN）。可打印的折纸地球仪模板——把地球展开成数学上可折叠的平面，28 条评论里全是「打印了，真好看」。
  • 手工设计的公交票据时代（2022） — When transit passes were designed by hand (2022)。87 分 / 28 评论（HN）。Letterform Archive 的 Milwaukee 公交票收藏——印刷设计史里被忽略的一角。
  • 雪豹神话 — The Myth of Snow Leopard。28 分 / 23 评论（HN )。拆解「Mac OS X 10.6 是最完美系统」的怀旧叙事——评论区一边考古一边吵「Snow Leopard 真的快吗」。
  • 读小说，忘掉其他一切 — Read the Novels and Forget Everything Else。21 分 / 5 评论（HN）。Hedgehog Review 的文学劝诫——在信息过载时代读长篇小说的价值论证。
  • Getting Started with Google Wave (2010) — Getting Started with Google Wave (2010)。△12 / 7 评论（Lobsters )。Google Wave 官方教程视频的考古——互联网产品史上最著名的「发布即巅峰」案例。
  • 你的网站呢？ — Where’s your website?。△21 / 19 评论（Lobsters )。个人网站复兴运动的又一宣言——19 条评论里一半在晒自己的主页。
  • Show HN: 让你的 Framework 12 听起来像一扇吱呀作响的门 — Show HN: Make your Framework 12 sound like a creaky door。33 分 / 2 评论（HN）。给可维修笔记本加「吱呀声」音效的项目——硬件黑客的幽默感，2 条评论都是「为什么」。
  • TinyNES 评测：一台超级小众的 NES 主机 — TinyNES Review – A Super Niche NES Console。16 分 / 1 评论（HN）。Lon.TV 对 TinyNES 的评测——2023 年的老视频重新上首页，复古硬件热度不减。
  • 我们教英语学习者的词汇如何改变 — How the words we teach English language learners changed。低分新帖（HN）。Pudding 的数据可视化：英语教材核心词汇表几十年的演变——数据新闻的典范，可惜在 HN 上没溅起水花。

📝 今日总结

今天的情绪线是「对 AI 的审视从结果转向了信任链」：Karpathy 宣布 pelican 基准毕业、有人开始按速度选模型，说明评测焦虑正在退潮；但 Lean 内核 soundness bug 被 LLM 证伪 Collatz 猜想的事件牵出，NetBSD 官方用「vulnpocalypse」形容 AI 带来的漏洞潮，两条新闻都在提醒：模型输出的可信度，取决于验证它的人/工具是否可信。必读 Top 3：① Karpathy 的 Pelican 帖（375 分，看评论区两派怎么吵基准饱和）；② Lean Soundness Bug #14576 事后分析（Lobsters 48 分，形式化验证信任链的第一手事故报告）；③ NetBSD 11.0 发布（Lobsters 99 分，RISC-V 支持 + vulnpocalypse 的坦诚发布策略）。横向信号：怀旧计算（6502 LLM、CP/M-386、MkLinux、RISC OS 20 年）与 AI 热潮同屏出现，复古硬件正在成为 AI 疲劳者的精神出口。