一句话：提出将 Alloy 模型编写与解探索交织的实时编程概念验证环境，改善开发者反馈循环。
有限模型查找器让用户用数学逻辑描述系统性质，并自动寻找满足性质的实例（解）。这些解本应帮助开发者探索模型，但实践中获益低于预期。过去研究者多认为问题是解过多；近期用户研究却表明用户偏好枚举较广泛的解集。基于对 Alloy（由有限模型查找器支持的建模语言）的用户研究，作者认为症结在于解与其逻辑约束过于割裂，难以帮助理解约束本身。本文提出一个面向 Alloy 的实时编程概念验证环境，将编写模型与探索解交织起来，并展示该环境如何在开发者、模型和解之间形成更高效的反馈循环。
Finite model finders give users the ability to specify properties of a system in mathematical logic and then automatically find concrete examples, called solutions, that satisfy the properties. These solutions are often viewed as a key benefit of model finders, as they create an exploratory environment for developers to engage with their model. In practice, users find less benefit from these solutions than expected. For years, researchers believed that the problem was that too many solutions are produced. However, a recent user study found that users actually prefer enumerating a broad set of solutions. Inspired by a recent user study on Alloy, a modeling language backed by a finite model finder, we believe that the issue is that solutions are too removed from the logical constraints that generate them to help users build an understanding of the constraints themselves. In this paper, we outline a proof-of-concept for live programming of Alloy models in which writing the model and exploring solutions are intertwined. We highlight how this development environment enables more productive feedback loops between the developer, the model and the solutions.