Become a Proofgrammer

Welcome to the world of Proofgrammers — where mathematical proofs meet Python programming! The term “Proofgrammer” is a delightful combination of “proof” (i.e., a precise explanation of the truth of a mathematical or computational statement) and “programmer” (i.e., the people who write software). As a proofgrammer, you’ll master the art of using Python to create, manipulate, and analyze proofs in the field of theoretical computer science. You’ll learn to express abstract mathematical concepts as concrete Python programs that can be run, tested, and verified. This course focuses on the theory of computation, exploring fundamental questions like “What can be computed?” and “What can be computed efficiently?” Whether you’re implementing Turing machines, analyzing algorithmic complexity, or proving undecidability results, proofgrammers use Python code to make theoretical concepts tangible and accessible. Want to learn more about the theory of computation? Join us as we explore how to be both rigorous mathematical thinkers and skilled programmers in the world of proofgramming!

Course Overview

With the goal of cultivating skilled proofgrammers, this web site features a sixteen-week schedule filled with activities that support the development of your professional and technical capacities in the field of theoretical computer science. Although this site is best used by an on-campus learner in the Department of Computer and Information Science at Allegheny College, the resources and projects are all publicly available. This course teaches you to harness Python’s power for expressing mathematical proofs and exploring theoretical concepts, from simple automata to complex undecidability results. You’ll learn to use tools like Jupyter Notebooks and Quarto to create interactive documents that blend theoretical proofs with executable Python code. Throughout the course, you’ll develop skills in implementing and analyzing algorithms, understanding computational complexity, and proving fundamental results in the theory of computation. In addition to learning more about version control, Git, and GitHub, emerging proofgrammers will also learn how to use artificial intelligence (AI) assistants GitHub Copilot, Google Gemini CLI, and OpenCode to create, revise, and extend both theoretical proofs and source code implementations. Check out the schedule and slides to begin your journey as a proofgrammer!

Python for Theory of Computation

As you explore the technical resources on this site, you’ll discover how Python can transform the way that proofgrammers work with theoretical concepts. Notice how proofgramming is practical, challenging, and fun! For instance, here’s a simple example of a Python implementation of a count_lines function that counts the number of lines in a source code file; it is an example of a computable problem. This function takes a file path, opens the file, and counts each line, demonstrating how we can algorithmically solve problems that have clear, step-by-step solutions. This represents the kind of computation that is always decidable and tractable. Notice that the website itself includes the output from running this function!

def count_lines(file_content: str) -> int:
    """Count the number of lines in the provided text content."""
    if not file_content:
        return 0
    lines = file_content.split('\n')
    return len(lines)

# example source code content
sample_code = """def hello_world():
    print("Hello, Proofgrammers!")
    return True

def main():
    result = hello_world()
    print(f"Function executed: {result}")

if __name__ == "__main__":
    main()"""

# count lines in the sample code
line_count = count_lines(sample_code)
print(f"Number of lines in the sample code: {line_count}")
print(f"This is a computable problem! we can always determine the line count!")

Number of lines in the sample code: 10
This is a computable problem! we can always determine the line count!

Now, let’s explore the fascinating world of universal computation! The following example demonstrates one of the most profound concepts in theoretical computer science: a universal program. This Python function executes another Python program, showing how one program can simulate any computation. This concept is fundamental to understanding the limits and possibilities of computation, and it’s directly related to Alan Turing’s work on universal Turing machines. Universal computation is what makes general-purpose computers possible and is essential to proving many results about what can and cannot be computed.

def universal(prog_string: str, input_string: str) -> str:
    """Execute a program given as a string on the provided input."""
    # create a local namespace for the program execution
    local_namespace = {}
    # execute the program definition to make the function available
    exec(prog_string, {}, local_namespace)
    # extract the main function from the executed program
    main_function = None
    for name, obj in local_namespace.items():
        if callable(obj) and not name.startswith('_'):
            main_function = obj
            break
    # execute the program with the given input
    if main_function:
        return main_function(input_string)
    else:
        return "No function found"

# example program that checks if a string contains "GAGA"
contains_gaga_program = '''
def contains_gaga(input_str):
    """Check if the input string contains GAGA."""
    if "GAGA" in input_str:
        return "yes"
    else:
        return "no"
'''

# example program that counts vowels in a string
count_vowels_program = '''
def count_vowels(input_str):
    """Count the number of vowels in the input string."""
    vowels = "aeiouAEIOU"
    count = sum(1 for char in input_str if char in vowels)
    return str(count)
'''

# demonstrate example of universal computation
test_string1 = "HELLO GAGA WORLD"
test_string2 = "programming"
print("Universal Computation in Action:")
print(f"Testing contains_gaga with '{test_string1}':")
result1 = universal(contains_gaga_program, test_string1)
print(f"Result: {result1}")
print(f"\nTesting count_vowels with '{test_string2}':")
result2 = universal(count_vowels_program, test_string2)
print(f"Result: {result2}")
print(f"\nThis demonstrates universal computation where one program simulates another!")

Universal Computation in Action:
Testing contains_gaga with 'HELLO GAGA WORLD':
Result: yes

Testing count_vowels with 'programming':
Result: 3

This demonstrates universal computation where one program simulates another!

Theory of Computation Resources

Ready to embark on your journey as a proofgrammer? Start exploring here:

• The sixteen-week course schedule provides detailed insights into each step that learners should take to emerge as skilled proofgrammers, including assignments focused on implementing theoretical concepts, analyzing computational complexity, and projects that combine proofs with programming.

• The course syllabus introduces the course and its learning objectives, explaining how on-campus learners will develop both their theoretical understanding of computational limits and their ability to use Python to implement and verify concepts from the theory of computation.

• The course slides offers links to the slides created by both the instructor and the proofgrammers who are learning more about theoretical computer science.

Proofgrammers Community Resources

Interested in connecting with other aspiring proofgrammers? Please join the Proofgrammers Discord Server and join the conversation about theoretical computer science, Python programming, and computational theory! If you are an on-campus learner at Allegheny College, you may also join the Allegheny College Computer Science Discord Server. Finally, if you are an on-campus learner, you can schedule an office hours appointment by visiting the Course Instructor’s Appointment Scheduler.