Budge: a programming language and a theorem prover

TL;DR

Budge introduces a simple G"odel-numbering-based programming language with scoped loops and a theorem prover relying on substitution and set equality, demonstrating their integration through examples.

Contribution

The paper presents a novel programming language and a minimalistic theorem prover, integrating them within a unified framework for formal reasoning and program evaluation.

Findings

Language syntax and semantics are clearly defined.

Theorem prover operates with simple substitution and set equality.

Examples demonstrate the language's and prover's capabilities.

Abstract

We present a simple programming language based on G\"odel numbering and prime factorization, enhanced with explicit, scoped loops, allowing for easy program composition. Further, we will present a theorem prover that allows expressing and working with formal systems. The theorem prover is simple as it relies merely on a substitution rule and set equality to derive theorems. Finally, we will represent the programming language in the theorem prover. We will show the syntax and semantics of both, and then provide a few example programs and their evaluation.