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

点击翻译按钮获取中文摘要

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.