Human Judgment as a Specification
The rise of GenAI in programming clearly requires an accompanying rise in formal methods, to confirm that AI systems running wild are producing the solutions we actually want. That in turn requires th...
评论
点赞
收藏通过空间细化来绘制程序值
编译器可以对您从未编写过的循环进行向量化。IDE可以在您完成之前就完成函数的编写。代理可以将您的代码库从一句话开始进行重构。然而，当您想要检查程序刚刚生成的值时，仍然像五十年前什么都没改变一样使用 REPL：输入一个表达式，获取返回的文本，眯起眼睛。这里，Python 为您展示了一个二进制决策图：节点(15, 'x1', 节点(14, 'x2', 节点(8, 'x3', TRUE, FALSE),...
负责任地使用LLM生成正则表达式
文章探讨了在使用生成式AI编写正则表达式时的风险与责任。作者指出，虽然LLM能生成正则，但直接复制粘贴存在隐患，如表述不清、领域歧义或模型误解。文章强调需要谨慎对待AI生成的代码，提倡负责任地使用GenAI，并引导读者查看后续更详细的博文以了解具体实践和背景。核心在于平衡效率与安全，避免盲目信任AI输出。
Why is cloud file-sharing hard? By analogy with programming misconceptions
Here is an actual situation we were asked to help non-technical computer users with: Alice and Bob want to collaborate on a flyer for a social event. They are more comfortable with Word than with clou...
面向隐私漏洞的实用静态分析方案
文章探讨了利用静态程序分析来发现隐私漏洞的难点。主要问题在于，为了让法律和合规专家能审核，分析规则不能写得太接近代码底层，需要在抽象度和可审计性之间找平衡。这导致构建有效的自动化工具面临挑战。
轻量级形式化方法的轻量级图表绘制工具
Brown PLT团队介绍了Spytial，这是其轻量级形式化方法可视化器的新版本。文章指出Alloy和Forge等工具的核心在于帮助用户定义、探索、验证和诊断复杂系统的规格说明，而可视化工具允许用户通过图形表示来探索生成的模型。Spytial旨在提供更轻量的图表绘制能力，以支持这一过程。
Argus：交互式调试 Rust 特征错误
Rust 的特征（Trait）错误信息以晦涩难懂著称。作者团队没有选择直接改进编译器报错，而是通过分析社区中真实的调试案例，找出工程师感到困惑的根本原因。基于这些认知工程学的假设，他们开发了一个名为 Argus 的交互式调试工具，允许开发者在 IDE 中逐步排查和解决复杂的 Trait 错误。文章介绍了这一研究过程及背后的论文。
有限轨迹与无限轨迹线性时序逻辑中的常见误区
文章探讨了线性时序逻辑（LTL）及其有限轨迹变体（LTLf）中常见的误解。作者基于过去三年与多国合作者的研究，深入分析了这两种逻辑在验证和机器人合成之外的应用潜力，如图像处理和网页技术。重点在于澄清概念混淆，帮助学习者更准确地理解和应用这些逻辑形式。
利用Transformer驱动反馈迭代优化学生编程计划
Brown大学PLT团队探讨如何利用LLM为编程初学者提供计划阶段的反馈。传统教学往往关注代码细节，而该研究主张在学生编写代码前，通过半形式化的计划表达来介入。早期研究尝试基于固定结构自动生成反馈，但最新项目显示这种方法存在局限。团队正在探索使用Transformer驱动的反馈机制，以更灵活、准确地评估学生的解题思路，从而在编码前纠正错误规划。这代表了编程教育中从语法纠错向思维过程指导的转变。
差分分析综述：起源、含义与后果
Brown PLT 团队回顾了过去几十年在差分分析（Differential Analysis）领域的工作。文章解释了该方法的起源、定义及其后果，并将其置于程序验证的背景中，即检查程序 P 是否满足属性 phi。这是一篇关于编程语言理论和形式化验证方法的历史与概念综述。
Examplar: A better way to teach programming (make students make the examples)
For the past several years, we have worked on a project called Examplar. This article summarizes the goals and methods of the project and provides pointers to more detailed articles describing it. Con...
Forge：一种教授形式化方法的工具
布朗大学PLT团队分享过去十年如何向非数学专业学生教授形式化方法。核心观点是形式化思维对构建系统的工程师至关重要。为此他们开发了名为Forge的教学工具，旨在降低入门门槛，将求解器等基于形式化的技术融入常规系统构建课程中。这是一篇关于计算机教育工具和方法论的经验总结。
发现并纠正关于程序行为的常见标准误解
文章指出Java、Python、JS等主流语言共享一个“标准模型”（词法作用域、急求值、可变变量、自动内存管理等）。作者通过Brown PLT博客的研究，揭示了开发者对这些基础语义的常见误解，并提供了修正这些误解的方法。这对深入理解语言底层行为、避免隐蔽Bug很有帮助，适合对编程语言原理感兴趣的工程师。
给编程语言学习做“体检”：一种新的教学法视角
文章提出将程序性能分析（Profiling）的概念应用于编程语言的学习过程。作者认为，就像程序员通过 Profiling 找出代码瓶颈一样，语言设计者和教育者也应该通过数据和分析来理解学习者如何掌握一门语言。这有助于优化文档编写和教学策略，提高语言 adoption。核心观点是引入数据驱动的方法来改进编程语言的普及和教育。
文档语言的核心演算：解决宏与变量设计的底层缺陷
文章指出Markdown、LaTeX等文档语言中的编程特性（如变量和宏）往往设计不佳，缺乏现代编程语言的标准（例如LaTeX宏系统不卫生导致冲突）。作者提出了一种新的核心演算（Core Calculus），旨在为文档语言提供更严谨、安全的底层理论基础，解决现有工具在复杂文档生成中的缺陷。
关于为学生设计程序规划记法的教学观察
Brown大学PLT团队分享在编程教育中的最新实验。他们尝试用高阶函数作为核心隐喻，教学生如何规划程序逻辑，并基于Snap!构建了工具支持。文章记录了从初步成功到在新学生群体中复现结果时遇到的挑战与反思，探讨了编程语言教学设计的实际难点。
概念变异测试：一种评估编程教学材料覆盖度的新方法
文章介绍了Examplar项目中的概念变异测试（Conceptual Mutation Testing）方法。这是一种针对编程教育中概念理解的教学评估技术。通过模拟学生对核心概念的常见误解来生成变异测试用例，从而检测教学材料是否有效地覆盖了这些关键概念。该方法旨在解决学生经常误解特定概念的问题，通过系统化地识别和测试这些概念盲区，帮助改进编程语言的教材和课程设计。
trivially生成程序：学生对大语言模型的使用现状研究
针对教育界对LLM生成代码的恐慌，布朗大学PLT团队的研究揭示了学生实际使用LLM完成编程作业的真实情况。研究指出，尽管部分机构全面禁止，但学生对LLM的使用远比预想的复杂和微妙。文章分析了学生如何利用LLM辅助学习而非单纯作弊，并探讨了这种工具对计算机科学教育模式的深远影响，呼吁从“禁止”转向“引导”。
Rust所有权类型的接地概念模型
Rust的所有权概念对传统程序员来说很难，是学习的主要障碍。本文提出了一种基于实证研究的 grounded conceptual model，旨在通过更直观的概念模型来解释Rust的所有权类型，降低学习门槛，帮助开发者更好地理解和掌握这一核心特性。