Budge: a programming language and a theorem prover
This work introduces a novel formal system for theorem proving and programming, potentially useful for researchers in logic and formal methods, though it appears incremental as it builds on existing concepts like Gödel numbering.
The authors developed a programming language based on Gödel numbering and prime factorization with scoped loops, and a theorem prover using substitution and set equality, then represented the language in the prover to demonstrate syntax, semantics, and example evaluations.
We present a simple programming language based on Gödel 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.