Language Embeddings for Proof Engineering

用于证明工程的语言嵌入

• 批准号: EP/Y000242/1
• 负责人: Alex Kavvos
• 金额: $ 12.42万
• 依托单位: University of Bristol
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY000242%2F1
• 关键词: Language; Embeddings; Proof; Engineering

There are certain kinds of computer systems and devices from which we demand impeccable performance: medical devices; air traffic control systems; railway signalling; self-driving cars. In such mission-critical systems anything less than perfect performance could amount to unimaginable losses.One way to certify a mission-critical system's behaviour is to produce a mathematical proof that it will function as expected. However, this approach merely replaces one problem with another: how can we then be sure that the proof is correct, especially when it may run to hundreds of pages of detailed technical arguments?To solve this problem we have developed proof assistants. These are remarkable pieces of software: not only can they help us build large proofs, but they can also check the correctness of a proof on our behalf. Thus, as long as we trust the kernel of the proof assistant, we have some assurance that our proof is correct (and hence that our system/hardware/software is bug-free).However, this solution is not perfect. Developing proofs is a challenging task, perhaps an order of magnitude more difficult than software development. This has led in the last 10 years to the creation of proof engineering, a new field of Computer Science which is concerned with the development of large mathematical proofs.In this project we aim to make foundational contributions to one popular aspect of proof engineering, namely the formulation of Domain Specific Languages (DSLs). We aim to show that practical DSLs developed and used by proof engineers can be given a solid footing using a field of mathematical logic known as type theory. Our results will lead to better, simpler, reusable, and more transparent ways to design DSLs. This will offer substantial benefits to proof engineers, who will then be able to employ our techniques in order to verify the safety of even larger mission-critical systems in a systematic fashion, and with less effort.The project will be carried out by combining the theoretical background of the PI in the semantics of type theory with the practical expertise of the international collaborator, who has previously crafted development tools for testing within a popular proof assistant, Coq

我们要求某些类型的计算机系统和设备具有无可挑剔的性能：医疗设备；空中交通管制系统；铁路信号；自动驾驶汽车。在此类关键任务系统中，任何不完美的性能都可能造成难以想象的损失。验证关键任务系统行为的一种方法是提供数学证明，证明它将按预期运行。然而，这种方法只是用一个问题代替另一个问题：我们如何才能确定证明是正确的，特别是当它可能长达数百页的详细技术论证时？为了解决这个问题，我们开发了证明助手。这些都是非凡的软件：它们不仅可以帮助我们构建大型证明，而且还可以代表我们检查证明的正确性。因此，只要我们信任证明助手的内核，我们就可以在一定程度上保证我们的证明是正确的（因此我们的系统/硬件/软件没有错误）。但是，这个解决方案并不完美。开发证明是一项具有挑战性的任务，可能比软件开发困难一个数量级。这导致了过去 10 年证明工程的创建，这是计算机科学的一个新领域，涉及大型数学证明的开发。在这个项目中，我们的目标是为证明工程的一个流行方面做出基础性贡献，即领域特定语言（DSL）的制定。我们的目标是证明，证明工程师开发和使用的实用 DSL 可以通过称为类型论的数理逻辑领域奠定坚实的基础。我们的结果将带来更好、更简单、可重用且更透明的 DSL 设计方法。这将为验证工程师带来巨大的好处，他们将能够利用我们的技术以系统化的方式验证更大的关键任务系统的安全性，并且花费更少的精力。该项目将通过结合PI 在类型理论语义方面的理论背景以及国际合作者的实践专业知识，该合作者之前曾在流行的证明助手 Coq 中制作了用于测试的开发工具