ProofScript

About

A custom programming language designed for verified algorithm development with built-in correctness checking and LaTeX documentation generation

Motivation

Inspired by formal verification methods learned in CS152, ProofScript was born from the frustration of manually proving algorithm correctness. The goal was to create a language that bridges the gap between algorithm design and formal proof, making it easier to write provably correct code. Built using Python with custom lexer/parser, implementing the visitor pattern for AST traversal, and achieving Turing completeness through careful implementation of control flow structures.

Key Achievements

• Designed and implemented a domain-specific language with custom lexer and parser achieving Turing completeness
• Built interpreter using visitor pattern for clean AST traversal and extensible node handling
• Implemented control flow structures (if/else, while, for loops) and array operations with proper scoping
• Solved complex grammar parsing issues through systematic debugging and architecture refactoring

Technologies Used

Python

Language Design

Parser Design

Visitor Pattern

Language Breakdown