Language Embeddings for Proof Engineering

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

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