Imperative programs from proofs

这个项目的目的是开发新的逻辑方法来从数学证明中提取程序。传统上，这类程序极其复杂，难以理解。我们将通过设计新的技术来改善这种情况，这些技术可以产生用更自然的语言编写的程序，从而使程序提取在目前应用的几个领域更加有效。背景：人们早就知道逻辑和计算之间有着很深的联系，数学证明可以转换成计算机程序。证明解释就是这样做的一种技术。它们有用的原因有很多。当在计算机中实现时，它们为我们提供了一种合成程序的方法，这些程序是按构造正确的，因此保证没有错误。当应用于复杂的数学证明时，它们有时可以揭示以前没有发现的新算法。现在有一个很大的逻辑子领域致力于使用证明解释从证明中提取程序。问题：证明解释是形式化的数学技术，因此它们通常会导致与人类编写的程序完全不同的程序。这些程序往往是用一种非常抽象的语言编写的，可能非常长，语法混乱，难以理解。这代表了将证明解释用于实际目的的一个缺点：虽然拥有一个我们知道完成特定任务的程序是有用的，但如果我们能够理解该程序是如何工作的，那将更有用！我的主要目标是：这个项目旨在使使用证明解释获得的程序更接近人类编写的程序。其目的是改进当前最先进的技术，以便用更自然的语言编写提取的程序，从而更容易理解。我的方法是：我们将采用所有证明解释中最强大和最广泛使用的解释之一——K. Goedel的辩证法解释——并对其进行调整，使其生成的程序在精神上更接近于现实世界的编程语言。这将涉及将全局状态与控制流语句（如while循环）合并在一起。这些都是C和Python等日常语言的核心功能，但在传统上与证明解释相关的理论语言中却没有。然后，我们将进一步完善新的解释，使其针对上面概述的两个主要应用进行优化：(i)合成按结构正确的程序，（ii）从复杂的数学证明中揭示有趣的新算法。这两个应用程序都需要不同的方法，特别是第二个应用程序将涉及数学逻辑中的许多深奥思想。然后，我们将通过开展一系列案例研究来展示我们的新技术，分别针对问题领域(i)和（ii），并针对将从我们的新方法中获益最多的特定社区。同时，我们将探索我们的新方法的泛化，以便它可能从编程中包含更多有趣的结构。该项目将要求我们将数学逻辑和编程语言理论的思想以及预期的应用（将通过我们的案例研究举例说明）结合起来，将形式验证和纯数学发挥作用。这使得该项目从根本上是跨学科的，我们将通过组织访问英国和国际上的一系列相关研究小组，并在项目结束时举办跨学科研讨会来利用这一点。

The aim of this project is to develop new logical methods for extracting programs from mathematical proofs. Traditionally, such programs are extremely complicated and difficult to understand. We will improve the situation by devising novel techniques that produce programs written in a more natural language, thereby making program extraction more effective in several areas in which it is currently being applied.Background: It has long been known that there is a deep connection between logic and computation, and that mathematical proofs can be converted to computer programs. Proof interpretations are a technique for doing this. They are useful for many reasons. When implemented in a computer, they provide us with a way of synthesising programs that are correct-by-construction and therefore guaranteed to be bug free. When applied to complex mathematical proofs, they can sometimes reveal new algorithms that have not been previously discovered. There is now a large subfield of logic dedicated to using proof interpretation to extract programs from proofs.The problem: Proof interpretations are formal mathematical techniques, and as such they often result in programs that are quite different from those a human would write. These programs tend to be written in a very abstract language and can be extremely long, syntactic, and difficult to understand. This represents a drawback to using proof interpretations for practical purposes: While it is useful to have a program that we know accomplishes a particular task, it would be more useful if we were able to understand how that program worked!My main goal:This project aims to bring programs obtained using proof interpretations closer to those a human would write. The aim is to improve the current state-of-the-art so that extracted programs are written in a more natural language and therefore easier to understand.My approach: We will take one of the most powerful and widely used of all proof interpretations - K. Goedel's Dialectica interpretation - and adapt it so that it produces programs in a language that is much closer in spirit to a real-world programming language. This will involve incorporating a global state along with control flow statements such as while-loops. These are all core features of everyday languages such as C and Python but are absent from the kind of theoretical languages traditionally associated with proof interpretations. We will then further refine the new interpretation so that it is optimized for the two main applications outlined above: (i) synthesising correct-by-construction programs, and (ii) revealing interesting new algorithms from complex mathematical proofs. These two applications will each require a different approach, and the second in particular will involve a number of deep ideas from mathematical logic. We will then demonstrate our new technique by carrying out a series of case studies, targeting problem areas (i) and (ii) respectively and aimed at specific communities who would most benefit from our new method. In parallel, we will explore generalisations of our new method so that it could potentially incorporate further interesting structures from programming.The project will require us to bring together ideas from both mathematical logic and the theory of programming languages, and the intended applications, which will be exemplified through our case studies, bring formal verification and pure mathematics into play. This makes the project fundamentally cross-disciplinary, and we will exploit this by organising visits to a range of relevant research groups in the UK and internationally, and by hosting a cross-disciplinary workshop towards the end of the project.