欢迎来到 Agili 的 Hacker Podcast，今天我们聚焦 Mozilla 的未来之路、AI 在开发领域的颠覆性应用、在线教育市场的巨变，并深入探讨软件开发工具与形式化验证的精髓。

一篇题为《Mozilla 是否正在努力自杀？》的文章在社区引发了对 Firefox 未来的深切担忧。文章作者对 Mozilla 新任 CEO 有关广告拦截器的言论表示高度怀疑。CEO 提到，禁用广告拦截器理论上可为公司带来 1.5 亿美元的额外收入，但他表示这“感觉偏离了使命”。作者认为这番话的潜台词是，为了钱，禁用广告拦截器依然是一个悬而未决的选项。他警告说，此举将疏远其核心用户群——那些关心隐私的技术爱好者，并可能成为压垮 Firefox 的最后一根稻草。

对于 CEO 的言论，技术社区的解读呈现出明显的两极分化。悲观者认为这是一种策略性的试探，甚至是在“待价而沽”。“感觉偏离了使命”的措辞显得软弱，而非坚定不移地捍卫核心原则。有人讽刺道：“你不会去计算禁用广告拦截器的预期回报，除非你真的在考虑它。”

然而，也有观点认为这是一种过于负面的解读，评估所有商业选项是任何 CEO 的职责所在。但即便是持这种看法的人也承认，CEO 的言辞不够坚定，缺乏对 Mozilla 核心价值的强烈捍卫。

一个强烈的共识是，广告拦截器是 Firefox 仅存不多的“杀手级特性”之一。许多人明确表示，正是因为 Firefox 对 uBlock Origin 等高效广告拦截器的良好支持，他们才选择留在这里。在当今恶意广告泛滥的网络环境下，广告拦截器不仅是体验问题，更是安全和隐私的保障。如果 Firefox 在这一点上向 Chrome 看齐，将失去其最后的阵地。

讨论也延伸到了 Mozilla 的长期困境。作为一个以开放、隐私为使命的非营利组织，其大部分收入却依赖于竞争对手 Google，这本身就是一种矛盾。大家呼吁 Mozilla 探索更多可持续的收入模式，例如通过订阅服务或优质功能，真正服务于用户而非广告商。许多人特别提到了 Firefox Mobile 在 Android 上对完整扩展（尤其是 uBlock Origin）的支持，这是其相较于 Chrome 的巨大优势，任何对这一优势的削弱都将是灾难性的。

AWS 首席执行官 Matt Garman 近日明确表示，用 AI 取代初级开发人员不仅不明智，还会对公司的未来造成严重影响。他认为，初级开发者往往更精通 AI 工具，能帮助资深同事掌握新技能；裁掉他们并不能带来显著的成本节约；最重要的是，这将破坏企业的人才输送管道，导致未来无人可用。

围绕这一观点，许多开发者表示赞同，认为 AI 实际上是初级开发人员的“加速器”。AI 能极大压缩学习曲线，帮助新人快速解决语法、API 调用和排错等基础问题，从而让他们能更快地接触到“大局观”的任务。有经验的工程师分享道，实习生在 AI 的帮助下能够迅速产出成果，推动项目进展。初级开发者也常常是团队中引入最新技术的先锋。

然而，也有一部分人对 Garman 的言论持怀疑态度，认为这可能是 AWS 在 AI 热潮中的一种公关说辞。对于 AI 的实际能力，许多质疑声指出，AI 仍是“低效的模版填充器”，容易产生“幻觉”，离真正“生产级”的自动化软件开发还有很长的路要走。

一些工程师观察到，部分初级开发者过度依赖 AI，虽然能快速生成代码，但自身对基础知识的掌握却不足，更多地扮演了 AI 输出的“人类过滤器”角色。还有观点讽刺地指出，许多公司只关注短期季度收益，10-15 年后的“人才管道”对他们来说是“别人的问题”。

谷歌 AI 部门发布了专为速度、效率和低成本打造的前沿模型——Gemini 3 Flash。它承诺以“Flash 级别的速度和成本，提供 Pro 级别的推理能力”，在多项基准测试中表现出色，甚至在某些编码测试中超越了更昂贵的 Gemini 3 Pro。谷歌将其定位为迭代开发、智能体编码和响应式交互应用的理想选择，旨在将强大的 AI 能力普及给全球数百万用户。

在技术社区，这次发布也激起了热烈的讨论，开发者们以其特有的热情剖析着这个新模型。

许多开发者对其性能印象深刻，称其为“新宠”，赞扬它的速度、广博的知识，并表示其性能在某些方面超越了其他顶尖模型，而成本却低得多。有用户报告称，在产品基准测试中获得了“疯狂的提升”，以三分之一的价格获得了更好的结果。甚至一些自称的“AI 怀疑论者”也因其能准确回答其他模型失败的刁钻问题而改变了看法。

尽管文章强调了成本效益，但一些细心的开发者指出，每代 Flash 模型的单位 token 价格实际上在上涨。不过，反驳的观点认为，虽然单位价格更高，但由于其卓越的性能和更高的效率（使用更少的 token），解决任务的“总成本”可能反而更低。大家也在猜测，谷歌未来是否会推出一款“Flash Lite”模型来填补超低价、超快速的生态位。

一个强烈的主题是 AI 竞争格局的转变。许多人认为谷歌正在“超越对手”，甚至有人断言 OpenAI 在通用聊天 AI 领域将面临巨大挑战。一些人批评 OpenAI 忽视了快速推理模型，而这种“一个模型通吃”的策略并未奏效。

谷歌新的“思考”等级（Thinking levels）引发了一些困惑。讨论澄清了“Thinking”实际上是 Gemini 3 Flash 的一个可配置的更高“思考等级”，允许调整推理深度。这也引向了更深层次的哲学讨论：这种“思考”与通用人工智能（AGI）有何不同？有观点详细分析道，尽管先进的 LLM 能够模拟智能，但它们仍缺乏 AGI 的核心属性，如一致性、真正的自学习、真实理解、自主性、持久集成记忆和意识。

此外，关于谷歌商业账户数据保留政策的讨论也浮出水面，开发者希望有更精细的控制。模型在处理近期信息时产生幻觉或对当前日期感到困惑的问题也再次被提及。最后，开源模型被视为对专有模型价格的一种制衡，虽然技术上落后几个月，但它们最终会达到对许多用例来说“足够好”的水平。

在线教育领域的两大巨头——Coursera 与 Udemy 宣布合并。这笔全股票交易旨在创建一个领先的技术平台，赋能全球劳动力掌握 AI 时代所需的技能。合并后的公司将结合 Coursera 在顶尖大学合作方面的优势和 Udemy 动态的技能市场，为个人和企业提供更广泛的学习选择，并加速 AI 原生创新。

这则合并消息引发了关于在线教育未来的广泛思考。

许多人提到，近年来 Coursera 和 Udemy 的内容质量都有所下滑。Coursera 从最初提供“顶级大学材料”的平台，变得内容质量参差不齐。一位在 Udemy 上有十年经验的资深讲师也发现，尽管他的课程评分很高，但平台却不再推广，导致销量锐减。这背后可能反映了平台算法对“新奇”内容的偏好，而经典、未经频繁更新的优质内容则被边缘化。

在线课程极低的完成率也备受关注。有数据称，50% 的购买者甚至没看完第一个视频，平均完成率仅为 5%。这引发了“买课程就像买健身房会员”的比喻，许多人购买的是一种“新开始的感觉”，而非真正的知识。这反映了在线平台虽然便利，但缺乏足够的结构和强制力来帮助学习者坚持下去。

关于“现代社会是否贬低旧知识”的讨论非常激烈。一方认为 IT 行业发展迅速，人们确实需要最新的信息。另一方则坚决反驳，指出许多核心基础知识，如线程安全、递归、操作系统原理、网络和数据库优化是永恒的。现代开发者有时过度依赖抽象层或新兴工具，缺乏对这些基础的理解，导致解决问题时效率低下。

AI 的兴起也改变了学习方式。有人宣称现在直接向 LLM 请求定制课程，但这引来了对“幻觉”问题的担忧，尤其是 LLM 编造不存在的论文引用。一种更稳妥的建议是，可以请 LLM 生成“自学大纲和参考资料”，利用其信息整合能力，同时通过查阅原始资料来规避幻觉风险。

浏览器 Waterfox 对 Mozilla 拥抱 AI，特别是大型语言模型（LLM）的战略转变表达了强烈不满。Waterfox 创始人认为，这是一个“根本性错误”。文章区分了有益的、透明的本地机器学习技术（如翻译）和作为“黑箱”的 LLM。它认为，将 LLM 集成到浏览器中，会使浏览器从用户的“代理人”变成“代理人的代理”，其行为不可预测且难以审计，这与 Mozilla 宣称的信任和透明原则背道而驰。Waterfox 表明立场，将继续为那些重视独立性和透明度的用户提供一个专注于浏览器核心功能的替代品。

围绕这一立场，技术社区展开了热烈的讨论。

许多人对 Waterfox 将本地机器翻译视为“好 AI”而将 LLM 视为“坏 AI”的立场提出质疑。技术上，两者都是基于神经网络的“黑箱”。真正的区别可能在于部署方式（本地 vs. 远程）、所有权（开源 vs. 专有）和数据访问权限。一个本地运行、功能受限的开源 LLM 应该比远程专有模型更值得信赖。Waterfox 的作者也在讨论中澄清，他更信任“受限的、单用途的、输出可部分验证的模型”，而非“能广泛访问浏览上下文的通用模型”。

关于浏览器内嵌的摘要功能是否真的有用，也形成了两派观点。支持者认为，摘要能帮助他们在面对长篇文章、视频或邮件时快速判断内容价值，提升效率。而反对者则担忧过度依赖摘要会损害阅读理解能力，摘要只是“缩短”而非真正的“总结”，可能会扭曲原文含义甚至产生“幻觉”。

对 AI 接入浏览器可能带来的数据隐私和安全问题，大家普遍表示担忧。如果 LLM 能够广泛访问用户的浏览上下文，可能存在数据泄露的风险。恶意网站甚至可能通过“提示注入”来诱导 LLM 泄露用户数据。AI 成为“用户代理的代理”的观点也得到了呼应，人们担忧 AI 在未经明确指令的情况下修改浏览记录或密码等敏感信息。

Simon Willison 展示了如何在短短 4.5 小时内，利用 AI 将一个纯 Python 实现的 HTML5 解析器库 JustHTML 成功移植到 JavaScript。这个实验的关键在于一个全面的、语言无关的测试套件和 AI Agent 的强大能力。他仅用几句指令启动 AI，之后在陪伴家人的同时，AI 不间断地运行，最终生成了 9000 行代码，通过了全部 9200 多个测试用例，成本仅为 20 美元。

这个令人惊叹的实验引发了对 AI 辅助编程的效率、伦理和未来的深入探讨。

一个广泛的共识是，健壮的测试套件是这次成功的关键。语言无关的测试标准为 AI Agent 提供了明确的目标和验证机制。这种“测试驱动开发”的模式非常适合 AI，因为它提供了清晰的反馈循环。未来，投入更多精力创建此类测试套件可能会变得越来越重要。

这是讨论中最激烈的部分。大多数人认为，AI 移植的代码仍是原始代码的衍生作品，应遵循原项目的许可证。然而，AI 生成内容本身的版权归属仍是一个法律灰色地带，尤其是在商业应用中，如果代码被证明侵犯了他人版权，可能会带来巨大风险。此外，也有人担心 AI 可能会“剽窃”开源工作，削弱贡献者的动力，甚至可能促使开源项目作者选择不公开其测试套件。

AI 是否会取代程序员的讨论再次浮现。一些人预测，未来几年大量编码工作将被 AI 替代。但更多人认为，软件工程师的角色将转变为更专注于理解复杂业务需求、系统设计、以及验证和重构 AI 生成的代码。能工作的代码和可维护、高质量的代码之间仍有差距，而这正是人类的价值所在。代码变得极其廉价，但设计“Agentic 循环”让 AI 有效工作的能力，以及评估和整合其产出的能力，将成为新的核心技能。

东北大学开设的一门新课程《软件开发工具入门》旨在填补传统计算机科学教育中普遍缺失的实践技能环节。课程围绕命令行、版本控制（Git）、构建系统（Make）和软件正确性（测试）四大模块展开，强调动手实践和理解工具背后的原理，培养学生自主学习的能力。

这门课程的设计理念在技术社区中获得了普遍认可，但其具体内容也引发了一些有趣的讨论。

一个普遍的观点是，这门课程与 MIT 著名的“计算机科学教育的缺失一课”非常相似，这说明这类“软件开发生存技能”的教学需求非常强烈。许多经验丰富的开发者都表示，如果他们在大学时能接触到这样的课程，将对职业生涯大有裨益。

对于课程内容的范围，存在一些争议。批评者认为，课程只停留在基础层面，缺乏对现代 DevOps、容器化（如 Kubernetes）、部署、监控等更高级工具的覆盖。他们认为，在当今时代，不具备 DevOps 思维的开发者不能算作真正的专业人士。

但支持者反驳说，这门课的定位是“入门”，面向低年级学生，其重点是传授基础知识和“如何学习”的方法，这比灌输一大堆特定工具更有价值。

课程中对构建系统 Make 的重点讲解也引起了讨论。一些开发者表示，在现代企业开发中很少遇到 Make，而更多地使用 Maven、Gradle、NPM 等工具。但也有许多人，特别是从事嵌入式开发的工程师，力挺 Make，认为它简单、通用，是理解所有构建系统背后“通用模型”的基础。

一篇富有洞察力的文章提出，我们可能用错了 AI。我们习惯于让 AI 进行创作，但其真正的超能力在于“消费”——阅读、理解和分析海量的人类无法处理的信息。作者将自己三年来数千条工程笔记、会议记录和思考洞察全部输入 AI，然后不再问“给我写点新东西”，而是问“我以前发现过什么？” AI 帮助他发现了被遗忘的模式、追溯了思想的演变，并将不同项目间的设计决策联系起来。AI 成为了他个人知识库的“终极读者”。

这一观点在技术社区引发了关于 AI 洞察准确性、隐私风险和未来应用的深刻思考。

对于 AI 生成的洞察，社区存在显著分歧。一些人分享了类似的积极体验，认为 AI 在某些方面甚至比自己的洞察更接近真实。即使是“低质量的摘要”，对于快速了解陌生领域也很有帮助。

然而，更多人表达了强烈的怀疑。他们指出，AI 会“幻觉”，且通常是“节略”而非真正的“总结”，这使得其结果难以验证。有观点认为，AI 的训练方式使其倾向于“说你想听的话”，而真正的总结需要高层次的抽象理解，这并非 LLM 的强项。一个令人担忧的例子是，AI 在总结医学术语时混合了大量不准确信息，甚至骗过了一位医学专业人士。

AI 强大的“消费”能力被许多人视为一把双刃剑。大家普遍担忧，政府和大型公司可以利用 AI 分析海量个人数据，预测或操纵行为，构建心理档案。这种“全景监狱”的概念，即无处不在的监控结合 AI 的实时分析，引发了对隐私和数字主权的深层忧虑。为了规避风险，在本地运行 LLM 成为一种被期待的解决方案，尽管目前仍面临硬件和技术挑战。

一篇关于 TLA+ 建模技巧的文章分享了一系列实用建议，帮助开发者更有效地利用这种形式化语言来设计和验证复杂的并发与分布式系统。其核心思想是以最少、最抽象的方式开始，逐步细化，始终专注于系统的核心行为和关键性质，如编写类型不变式（TypeOK）、尽可能多地编写其他不变式和进展属性，并对模型检查的成功保持怀疑。

大家普遍认同 TLA+ 是一个强大的工具，尤其在分布式系统设计中能提供数学上的严谨性。然而，在团队中推广却面临阻力，其陡峭的学习曲线也是一个反复被提及的痛点。学习 TLA+ 不仅需要掌握新语法，更需要培养抽象思维。不过，一个乐观的看法是，在 AI 时代，LLM 有潜力帮助减轻语法上的痛苦，降低上手门槛，可能使其应用更加普及。

一个精彩的讨论围绕着“如何为像 Google Docs 这样的协作编辑系统定义不变式”展开。开发者们迅速列举了大量可能的属性，例如：

这个例子生动地展示了如何将复杂的现实世界问题分解为一系列可以用形式化方法验证的属性。

Dafny 是一种“验证感知”的编程语言，它原生支持在代码中编写规约（specifications），并配备了一个强大的静态程序验证器。这意味着开发者不仅能编写代码，还能用数学方式证明代码的正确性，在编译阶段就捕获那些传统测试难以发现的缺陷。Dafny 代码可以编译成 C#、Java、Go 等多种主流语言，旨在将形式化验证的严谨性带入日常开发流程。

关于“为什么不直接验证现有语言（如 C++ 或 Java）”的疑问，讨论给出了深刻的见解。我们常用的编程语言在某些方面“表达力不足”，难以清晰地编写规约；而在另一些方面又“过于自由”，例如允许使用难以验证的非类型化指针或复杂的内存管理，这使得严格的形式化分析变得极其困难。

Dafny 这样的专业语言通过提供更丰富的规约语法，同时对代码实现施加更多限制，从而简化了验证过程。它强制用户定义前置条件、后置条件和循环不变式等关键属性，使得编译器可以在编译时就防止你创建违反这些规约的代码，除非你能提供相应的数学证明。

与其他类似工具相比，Dafny 更侧重于教学和非实时应用，其多语言编译目标使其能很好地与现有生态系统集成。而像 SPARK (Ada 的子集) 则更多用于安全关键和实时嵌入式系统。与 Eiffel 的运行时检查相比，Dafny 的优势在于可以在“构建时”对更复杂的不变式进行静态证明。Dafny 代表了软件开发中追求更高可靠性的一种重要方向，尽管它要求开发者掌握新的思维模式，但其在早期捕获错误的潜力对于构建高可信度系统具有深远意义。

相关链接：

• Is Mozilla trying hard to kill itself?
• AWS CEO says replacing junior devs with AI is 'one of the dumbest ideas'
• Gemini 3 Flash: Frontier intelligence built for speed
• Coursera to combine with Udemy
• No AI* Here – A Response to Mozilla's Next Chapter
• I ported JustHTML from Python to JavaScript with Codex CLI and GPT-5.2 in hours
• Introduction to Software Development Tooling (2024)
• AI's real superpower: consuming, not creating
• TLA+ Modeling Tips
• Dafny: Verification-Aware Programming Language