FMitF Track I: Formal Methods in Software Support for Sound Experimentation

实验是了解世界的重要工具。实验无处不在，无所不在，而且常常是理解因果关系所必需的。每当一个人学习如何与新手机互动，或者试图理解为什么我们的汽车无法启动时，他就会进行非正式的实验。作为个体，人们会为自己进行实验，但组织也会进行实验，以了解产品、政策或设计决策对许多客户、公民和用户的影响。随着人们的手机、智能设备和社交媒体平台越来越多地以软件为媒介，一个人的实验能力既受到软件的驱动，也受到软件的限制。不幸的是，在编写软件时通常不会考虑到对实验的支持。这严重限制了人们理解复杂因果关系的能力，比如新闻提要算法在用户对当前事件的理解中所起的作用。该项目将开发工具和技术，使软件实验更容易、更透明，同时不牺牲灵活性和正确性。目前软件实验还没有一个统一的框架；虽然有库、配置语言和服务可以为实验提供有限的支持，但很少有像日志框架这样的端到端系统。相反，开发人员通常必须编写定制的软件，导致系统(a)为特定任务量身定制，(b)与假设和分析脱节。这个项目将为实验产生一个高级领域特定语言（DSL），它根据实验设计的基本原则对假设、分析和处理分配施加约束。用这种语言编写的实验将是正确的，因为它的结构与假设的一致性和处理任务的可识别效果有关。然后，该团队将把实验DSL集成到用于教育的传统社会技术软件中，利用现有的渐进式类型支持来实现实验干预的正交类型系统。为了评估这些工具并促进围绕实验分析管道的正式方法方法的持续研究，该团队将建立一个公开可用的可搜索的实验存储库。该项目由该领域的正式方法和促进竞争研究的既定计划（EPSCoR）共同资助。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Experiments are a critical tool for understanding the world. Experimentation is ubiquitous, pervasive, and often necessary to understand the relationship between cause and effect. Every time one learns how to interact with a new phone or try to understand why our cars will not start, one informally experiments. As individuals, people experiment for themselves, but organizations also experiment to understand the effects of products, policies or design decisions for many customers, citizens and users. As the world is increasingly mediated by software through people's phones, smart devices, and social media platforms, one's ability to experiment is both driven and limited by software. Unfortunately, software is not often written with support for experimentation in mind. This severely limits one's ability to understand complex cause and effect relationships, such as the role that a news feed algorithm play on users' understanding of current events. This project will develop tools and techniques for making experimentation in software easier and more transparent, without sacrificing flexibility or correctness. At present experimentation in software has no unified framework; while there are libraries, configuration languages, and services that can provide limited support for experimentation, there are few end-to-end systems in the style of e.g., logging frameworks. Instead, developers must typically write bespoke software, resulting in systems that are (a) tailored to a specific task and (b) disconnected from hypotheses and analyses. This project will produce a high-level domain-specific language (DSL) for experimentation that enforces constraints on hypotheses, analyses, and treatment assignment according to the underlying principles of experimental design. Experiments written in this language will be correct by construction vis a vis consistency of hypotheses and treatment assignments with respect to their identifiable effects. The team will then integrate the experimentation DSL into legacy socio-technical software for education, leveraging existing support for gradual typing to implement an orthogonal type system for experimental interventions. To evaluate these tools and promote continued research around formal methods approaches to the experimentation-analysis pipeline, the team will build a publicly available searchable experiment repository. This project is jointly funded by Formal Methods in the Field and the Established Program to Stimulate Competitive Research (EPSCoR).This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.