TLA+ 擅长设计并发系统并验证不变量、动作属性、活性和精化，但无法解决智能体软件开发中的所有问题。只有当开发者能够准确表达所需属性时，形式化验证才有效。 原生 TLA+ 规范通常难以表达多步行为、浮点数或实时相关问题、存在性可达性（“这种结果有可能发生”）、用于比较多种执行轨迹的超属性，以及针对整个状态空间的元属性。一些重要需求，例如证明游戏可以获胜、比较不同模式的能耗，或检查统计性能，可能都超出了它的表达能力。 有些缺口可以通过辅助变量、自组合、公平性、机器闭包，或 `REACHABLE` 和 `TLCGet` 等 TLC 扩展来近似解决。然而，这些技术可能使模型复杂化、破坏精化，并导致状态空间爆炸。CTL 和 PRISM 等其他工具支持不同类型的属性，但也有各自的权衡。 TLA+ 可以有意义地检查“凭感觉编程”的系统，尤其适合处理容易发现且收益明显的并发和可靠性属性，但它无法表达或验证所有性质。
每日HackerNews RSS
TLA+ 擅长描述时序不变量，并对系统设计进行模型检查，但模型验证通过并不代表实现符合相应规范。这种规范与代码之间的落差仍是其主要局限。
PlusCal/TLA+ 的语法往往较为别扭，而且涉及编译器或 CPU 重排序的弱内存行为必须手动建模。可行的衔接方式包括生成基于属性的测试、进行运行时轨迹验证，以及使用 SPARK、Dafny、Frama-C、Miri、Loom 和 GenMC 等工具作为补充。直接从形式化规范生成实现仍大多处于实验阶段。Quint 则因更易上手且采用类似 TLA+ 的风格而受到好评。
参与者对内存排序指南存在分歧：顺序一致性可以简化推理，而无锁编程领域的专家则认为，较弱的排序方式在很多时候是必需的，并且必须经过严格验证。
大语言模型可以帮助起草规范和实现，但无法可靠地确认代码与规范是否一致，也无法选出所有相关属性。总体而言，TLA+ 的价值在于澄清设计和发现缺陷，而不是保证生产代码正确。
Bild AI 是一家以社会影响为驱动的初创公司，致力于将先进的计算机视觉和人工智能技术应用于图纸解读、成本估算及许可申请，帮助建筑行业建设更多住宅、医院和学校。 我们正在招聘一名全栈、从 0 到 1 的产品工程师，由其端到端负责各项功能：每周访谈客户，将复杂的建筑工作流程转化为清晰的产品决策，参与制定产品路线图，并快速交付产品。你将横跨 React 前端、Python 后端和基础设施，为经验丰富的行业专业人士打造简单、直观的界面。 理想的候选人应具备优秀的产品判断力、扎实的全栈技术能力，能够直接与客户沟通，并富有同理心、诚实、成长型思维和出差意愿。招聘流程包括：15 分钟介绍、一小时白板技术面试、一小时编程面试，以及 3 至 5 天的带薪试岗。该职位为全职、坐班制，工作地点位于旧金山，接受异地搬迁申请。
```
Hacker News
最新
|
往期
|
评论
|
提问
|
分享
|
工作
|
提交
登录
Bild AI（YC W25）正在招聘一位创始产品工程师
（
ycombinator.com
）
1 天前
|
隐藏
指南
|
常见问题
|
列表
|
API
|
安全
|
法律
|
申请加入 YC
|
联系我们
搜索：
```
在使用 AI 编写代码之前，我会为重大改动撰写详细的提交说明，解释改了什么，更重要的是说明为什么改。这需要重新阅读并评估代码，常常还会带来改进，同时把关键的推理保留给后来的读者。 AI 生成的提交说明带来了一种新的风险：智能体可能不了解对话、项目工具或未记录决策中的上下文，于是编造看似合理的理由。给智能体提供更多上下文可以降低这一问题，但无法验证代码是否真的实现了提交说明所声称的内容。 因此，自己撰写提交信息仍然很有价值。它会迫使我审查改动、确认其目的，并识别出那些可能只存在于我脑海中的临时决策和退出条件。如果我无法解释为什么要做某项改动，那我可能并没有真正理解它，或者还没准备好交付它。即使代码由智能体编写，亲自写下变更原因仍然是一种必要的思考和验证方式。
《The Hacker News》上的一则讨论将提交说明视为一种思考工具，而非事务性工作。撰写提交信息，尤其是解释“为什么要这样改”，可以暴露知识盲点、揭示隐含假设、厘清替代方案，并避免糟糕决策演变成技术债。有些开发者会在编码前先写提交信息、PR 描述、ADR 或 AI 提示词，以便更好地理解并掌控自己的改动。
AI 可以通过质疑假设、研究背景、提供信息来源或起草待修改的文本来提供帮助。然而，将整个过程完全交由 AI，可能产出空泛或冗长的描述、虚构的改动动机，以及脆弱的实现。提交信息应记录无法从代码中推断出的业务背景或历史背景；具体做了什么，通常可以从 diff 中看出。
参与者对于“写作本身是否就意味着思考”存在分歧。有些人认为，即使是不完美的写作也能改善推理；另一些人则表示，重复且不经思考的写作只是机械劳动。总体而言，讨论更倾向于由人主导，并对改动原因作出简洁说明。
卡内基梅隆大学宣布获得肯尼·格里芬30亿美元的历史性捐赠 Carnegie Mellon University Announces Historic $3B Gift from Ken Griffin
2 天前
卡内基梅隆大学宣布，Citadel创始人兼首席执行官肯·格里芬向该校捐赠30亿美元，这是高等教育史上金额最大的个人捐赠。此次捐赠包括10亿美元用于卡内基梅隆大学匹兹堡校区，其中5亿美元用于学校重点事项，5亿美元用于计算机科学学院；该学院将更名为“肯尼斯·C·格里芬计算机科学学院”。格里芬还将加入卡内基梅隆大学校董会。 其余20亿美元将用于建设卡内基梅隆大学迈阿密校区。该校区位于温伍德，占地35英亩，将围绕社会挑战而非传统学科专业进行设置。其初期研究重点包括人类健康、国家安全、能源与气候韧性，以及先进制造。这所跨学科校区将融合教育、研究、产业合作、创业工作室，以及人文学、艺术和设计。 校区计划于2027年动工，并在获得监管批准后，预计于2028年迎来首批学生。建成后的校区预计可容纳超过3,500名学生、300名教职人员和600名工作人员。这笔捐赠还将推动卡内基梅隆大学扩大全球影响力、吸引顶尖人才并应对紧迫国家挑战的更广泛战略。
一个 Hacker News 帖子讨论了卡内基梅隆大学据报道获得凯文·格里芬 30 亿美元捐赠的消息，其中包括约 20 亿美元用于在迈阿密建设新校区，以及 10 亿美元用于计算机科学和匹兹堡的设施。
评论者意见分歧。支持者强调这笔捐赠对教育、研究和学生的巨大益处，并指出大学经常以某种方式表彰大额捐赠者。批评者则质疑格里芬对校园治理、学术自由、课程设置和学校声誉的影响，尤其考虑到佛罗里达的政治环境。他们还将格里芬的动机和权力与安德鲁·卡内基、安德鲁·梅隆等历史人物相提并论，同时认为富有捐赠者正越来越多地利用大学建立个人遗产并施加社会影响。
其他讨论主题包括：卡内基梅隆大学的迈阿密校区能否成为成功的创业中心；冠名权是否比人们承认的更重要；精英大学是否正在吸纳与其规模或社会影响不成比例的财富；以及对格里芬动机的猜测。一段较长的子讨论还围绕格里芬在伊利诺伊州和芝加哥的政治活动展开，但其中很多内容逐渐变成了党派化和个人化的讨论。
Gitea 28.0.0 现已发布，不再沿用历史上的 `1` 前缀。这个以安全为重点的版本新增了审计日志、机器人账户、管理员用户模拟、用于 HTTPS 的部署令牌、CODEOWNERS 审批强制执行、差异搜索和扩展名过滤，并改进了关注选项、仓库切换、模板排除、许可证检测和 Actions 体验。Actions 新增或改进了队列、工件预览、动态矩阵、`max-parallel` 以及扩展 API。
升级人员应查看破坏性变更、备份数据，并替换二进制文件或容器。必须使用 Git 2.25 或更高版本。已完成的 Actions 运行记录、日志和工件默认在 400 天后删除；如需永久保留，请先将保留期限设置为 `0`，然后再升级。
除非明确启用，否则用户自行注册功能处于禁用状态；`DOMAIN` 已被 `ROOT_URL` 取代，SSE 已被 WebSockets 取代，Git 操作现在使用内部出口代理。请检查严格的出口允许/阻止列表以及已弃用的迁移设置。作业级别的 `if`、快速失败行为和可复用工作流权限规则均已更改。
发布二进制文件不再包含 32 位 x86 或 gogit 构建，armhf Snap 构建已停止，下载文件名也已更改。反向代理必须支持 WebSocket 升级；多进程部署需要使用 Redis 发布/订阅。
Hacker News 上的讨论介绍了 Gitea 28.0，并将 Gitea 与 Forgejo 进行了比较。评论者指出，许多开发者只需要一个裸 Git 远程仓库，而其他人则看重 Gitea 或 Forgejo 提供的 Web 界面、访问控制、问题跟踪和内置 CI/CD 功能。对于 Forgejo 这个分叉项目，各方意见不一：支持者认可它的治理方式和开放性；批评者则认为这次分裂没有必要，或者指出 Gitea 仍在积极开发，同时存在对半开放核心模式的担忧。相比营销宣传，发布说明和项目中可观察到的健康状况被认为更适合作为决策依据。
另一场争议涉及 Gitea 延迟公布安全修复细节，显然是为了给管理员留出升级时间。批评者认为这样做带来的优势有限，因为攻击者可以立即检查补丁，尤其是在 AI 辅助分析的情况下。Gitea 项目负责人表示，这项政策沿用了 PeerTube 的做法，也反映了维护者的反馈。
讨论最后以玩笑收尾：Gitea 去掉了版本号中的“1.”前缀，从 1.27 直接跳到了 28。
在 2026 年 9 月 25 日发布的一份披露中，研究人员 Faav 报告了微软内部 Titan 分析服务的一个严重漏洞。Titan 会接受带有微软兼容的租户、受众、应用程序和用户声明的 JWT，却不验证其加密签名。Faav 将未签名令牌的 `upn` 声明设置为 `admin`，从而获得了该服务的本地管理员身份以及未授权的 SQL 查询权限。
该漏洞暴露了 17 个分析数据库中的 30 个活跃路由目标，这些数据库估计包含 17.3 万亿条存储记录和 9,863 个不同的表。可访问的元数据包括约 25,000 个应用账户和 17,990 条员工电子邮件记录。Faav 还通过两次受限的单行采样确认了能够访问 Bing 分析服务，但他没有导出数据集、识别用户、关联记录、访问个人身份信息（PII）或证明实际利用了该漏洞。
Faav 于 9 月 5 日向微软报告了此问题；微软在 9 月 9 日前禁用了相关端点，并授予了 5,000 美元的奖金。该文章还指出，微软在发布前编辑了披露内容，以削弱或重新表述部分有关影响范围的声明。
一名16岁的安全研究员披露了一个漏洞，可能导致约17 TB的微软记录暴露，其中包括住客登记和身份信息。微软向其支付了5,000美元，据称还要求对文章拥有编辑控制权，删减了部分内容，并淡化了漏洞的影响。
Hacker News 的评论者普遍称赞这位研究者的技术能力、成熟度和清晰的写作 Many 人批评微软的安全实践、组织 priorities，尤其是漏洞赏金过低，认为这种规模的漏洞应当获得接近10万美元或更高的报酬。另一些人指出，未成年研究者可能会非常看重声誉、指导、工作机会以及未来参与漏洞赏金项目的机会，因此5,000美元也可能是一笔值得接受的报酬。
这个漏洞涉及错误地接受使用 `alg: none` 设置的无签名 JWT。评论者们讨论了责任究竟在于微软的实现、JWT 容易出错的设计，还是两者兼有，并建议采用更严格的内部安全标准，例如微软的 MISE 框架。
讨论还涵盖了负责任的披露、担心遭到法律报复、漏洞赏金市场萎缩、AI 辅助写作，以及在黑市出售漏洞的伦理问题。总体而言，舆论强烈支持这位研究员，并对微软提出了尖锐批评。
Gemini 4 Argon（高配）：智能水平、性能与价格分析 Gemini 4 Argon (High): Intelligence, Performance and Price Analysis
2 天前
Gemini 4 Argon（High）是智能水平领先的模型之一，与同价位的大多数模型相比价格也较为合理。该模型支持文本和图像输入，输出文本，并提供 100 万 token 的上下文窗口。 Gemini 4 Argon（High）在 Artificial Analysis 智能指数中的得分为 53，在同类模型中明显高于平均水平（中位数为 26）。在智能指数评估过程中，该模型生成了 1.1 亿个 token，相比 8200 万的中位数略显冗长。 Gemini 4 Argon（High）的价格为每 100 万输入 token 2 美元（价格适中，中位数为 2 美元），每 100 万输出 token 10 美元（价格适中，中位数为 10 美元）。在智能指数评估中，评估该模型完成每项任务的平均成本为 1.99 美元。
关于 Google Gemini 4 Argon（High）的 Hacker News 讨论褒贬不一。Artificial Analysis 的结果显示，它的智能水平接近前沿，单任务成本与 GPT-6.1 Sol 和 Claude Opus 5.5 High 大致相当，但价格低于更昂贵的“Max”档模型。Google 的首发定价为每百万输入 token 2 美元、每百万输出 token 10 美元，并提供缓存输入折扣；业内普遍认为这一定价颇具进攻性。
支持者强调，它在基准测试中的效率很强，据报道幻觉率较低，并具备多模态能力。此外，Google 垂直整合的基础设施，以及 Search 庞大的 token 用量和 Cloud 分发渠道，也为其提供了优势。这些因素可能对 OpenAI 和 Anthropic 构成压力，尤其是在 AI 威胁 Google 搜索广告业务之际。
质疑者则认为，Argon 并非智能水平上的重大突破，仍逊于 Anthropic 和 OpenAI 的顶级配置，也可能延续 Google 偏重优化基准测试、而非可靠实际表现的倾向。还有人称，Gemini 模型在编程、一致性和智能体任务方面表现不佳。此外，Argon 何时公开可用、订阅配额如何，以及模型是否存在被官方“暗改削弱”的情况，也尚无定论。
总体而言，评论者认为 Argon 是一款可信且可能带来颠覆的发布，但在日常使用中是否明显更优，尚未得到证明。
一场 Hacker News 讨论赞扬了彭博终端（Bloomberg Terminal）作为专家优化界面的优势：简洁、信息密度高、由键盘驱动，并旨在支持快速浏览和操作。评论者认为，它优于航空电子设备、任务控制中心和工业系统；同时，他们批评现代消费级图形界面过度重视新手易用性，却忽视了专家效率、稳定性和肌肉记忆。
彭博终端整合了实时及历史金融数据、新闻、分析工具、交易、专业通信和强大的人工支持。其功能广度、可定制性、数据质量以及网络效应，使其很难被替代，尽管市场上也存在其他选择。
其他人还讨论了它每年约 2.5 万至 3.2 万美元的价格、有限的公众访问权限、身份象征意义、垄断力量，以及此类工具可能加剧金融不平等的问题。技术讨论涵盖其发展历史、专用键盘和字体，以及基于 Chromium、TypeScript、C++ 和其他语言的现代实现，其中还包括一套基于 OCaml 的衍生品定价领域特定语言。
Halfspace 是一款实验性的跨平台 IDE，使用距离场进行实体建模，并基于 Fidget 几何内核构建。它支持基本几何体、手写的 Rhai 脚本、增量式模型组合、实时可视化，以及导出为图像或三角网格。传统 CAD 通常会隐藏距离场，而 Halfspace 强调物理上可实现、具有明确内外边界的实体。
Halfspace 不将距离场封装在构造实体几何运算中，而是直接公开场值和梯度。这有助于用户诊断不连续和行为异常的边界，因为这些问题可能导致法线或着色错误，或影响网格质量。
该应用使用 Rust、egui、wgpu、Rayon、WebAssembly 等库，可在原生环境和浏览器中运行。它也推动着 Fidget 的开发：GPU 加速的光栅化和着色现已使 Web 端具备交互性能。渲染逻辑集中在 Fidget 中，Halfspace 仅保留精简的着色器。
Halfspace 仍处于实验阶段，可能会进行破坏性 API 变更，不适用于关键工作负载。项目采用 MPLv2 开源许可证，并欢迎在 GitHub 上提交问题和参与讨论。
关于 **Halfspace** 的 Hacker News 讨论。Halfspace 是 Matt Keeter 用来通过距离场进行实体建模的实验性 IDE。评论者提到，Keeter 长期从事独立研究，并分享了他的研究档案、论文以及一场关于隐式曲面的演讲。
讨论随后延伸到独立研究面临的挑战：如何在没有机构支持的情况下建立结构和社区、如何维持自主规划的职业道路，以及如何兼顾工作中的创造性与实用性。有人还将 Kartik Agaram 的 **Mu** 作为类似的独立项目加以举例。
几位评论者分享了相关工具，其中包括一款基于 WebGL 的 SDF 编辑器，它支持输入 ShaderToy 代码，并能导出用于 3D 打印的 STL 文件。还有人称 Halfspace 是 **Antimony** 的精神传承者，表达了自己试用它的强烈兴趣，并开玩笑说要等待“ Halfspace 3”。
Netlify 重建了其 Edge Functions 平台，在自有边缘网络中运行 Firecracker MicroVM，不再依赖托管执行服务。温调用延迟的中位数从 25–40 毫秒降至约 5–6 毫秒，速度提升约五倍，同时改善了可用性、安全性、韧性和日志交付能力。
请求会在距离最近的边缘节点终止 TLS，获取带版本信息的机器规格，并通过 Rendezvous 哈希路由到计算节点。各服务按部署进行隔离，防止代码或配置更改共用 MicroVM。计算节点会缓存函数镜像，并使用内存映射 EROFS 文件系统、快照和缩容至零机制来减少冷启动开销。本地 DNS、详细的性能指标、断路器、独立的计算节点集群，以及基于健康状况的控制平面滚动部署，共同提升了可靠性和部署安全性。
此次迁移无需客户更改任何代码、配置、价格方案或工具。新架构还为支持更多 npm 包、提高资源上限，以及推出过去依赖第三方基础设施的新功能创造了条件。
Netlify 重建了 Edge Functions 平台，取代了托管在外部的 V8 isolate，换成运行在自身网络中的、基于 Unikraft 的 Firecracker MicroVM。Netlify 表示，这样做后中位延迟大约降低了 5 倍；借助预先预热的 MicroVM 快照，JavaScript 服务器的启动时间约为 15 毫秒，冷启动也只略慢一些。
评论者认为，这一标题具有误导性：V8 isolate 通常具有更低的启动开销和更好的资源效率，而报告中延迟改善的主要原因是消除了与外部执行提供商之间的网络跳转，并非 MicroVM 本身运行得更快。
主要优势在于更强的隔离性。V8 isolate 共享进程、内存空间、分配器和内核，因此不被视为严格的安全边界。MicroVM 拥有独立的内核和硬件虚拟化机制，更适合运行不受信任或对安全性要求较高的代码，但也会增加复杂性、资源成本，以及与快照相关的潜在安全问题，例如重复的随机数生成器状态。
讨论还涉及 Firecracker 的替代方案，包括 SlicerVM 和 smolvm、AWS 在创建 Firecracker 中的作用，以及对 Netlify 或 Unikraft 利用此次发布进行推广的质疑。