Brandon Sayler, COL ’25, Chandler, AZ
This summer, I had the wonderful opportunity to learn about Programming Languages research, guided by the expertise of Penn Professor Steve Zdancewic and PhD student Stephen Mell. My experience was enriched not only by their mentorship, but also by the collaborative environment created by PhD students Joey Velez-Ginorio and Cassia Torczon for Penn’s Research Experience for Undergraduates in Programming Languages (REPL).
Coming into the summer, I knew very little about the field of programming languages. What drew me to the field was a newfound interest in formal verification—a field that concerns proving mathematical statements by writing computer programs. Instead of painstakingly demonstrating mathematical proofs via traditional pen and paper, we can succinctly express them in code. This process involves writing propositions and employing formal methods to verify them. The validation occurs within our computer code: if it compiles successfully, our proof holds.
Why should we care about proving things with computers? The sheer length and complexity of mathematical proofs can be overwhelming—some proofs span hundreds of pages. For mathematicians, having these proofs verified by machines can save tons of time, simplifying the overwhelming task of peer review. Moreover, interactive theorem provers, the software we utilize for these proofs, significantly enhance the proving process by providing real-time feedback and corrections. Research is also progressing in the subfield of automated theorem proving, especially with the use of AI, such as a recent breakthrough made by Google DeepMind in July 2024.
We can also apply these formal verification techniques to the code we write—any of the code we write—to prove that it is safe and bug-free. The ability to prove that our code functions as intended is not merely a theoretical exercise; it’s a necessity in software development where reliability is paramount. This is especially true in fields such as cybersecurity, where small bugs can cascade and lead to dire consequences. There’s also been significant recent interest in the use of verification to formally prove that current and future AI systems are safe, explainable, and trustworthy.
As the summer began, I quickly realized that the discipline of programming languages encompasses much more than just this singular focus. The exposure to design and implementation processes of different programming languages broadened my understanding and appreciation of the field. I was particularly enlightened by the rich theoretical framework of lambda calculus, a universal model of computation that can help us reason effectively about programming languages.
Over the course of the program, working with an interactive theorem prover called Coq was particularly rewarding. I spent four weeks mastering its intricacies before transitioning to a six-week project in intersection of programming languages and artificial intelligence. My goal was to develop a parallelized Python library for LLM prompting—a challenging yet gratifying endeavor. The mentorship I received from Steve and Stephen was invaluable. Their encouragement allowed me to ask questions freely and explore difficult concepts without hesitation.
One of the most enriching aspects of the REPL program was the camaraderie built among the interns. I was blown away by their insights, passion, and experience, and I couldn’t imagine a better group of people to spend the summer doing research with. I also had a blast sharing the love I have for the City of Philadelphia with them, the apex being a karaoke night in Chinatown.
My summer was a completely transformative experience, and I’m so grateful that Career Services was able to fund this opportunity. I am now more inspired than ever to continue exploring this domain, equipped with new knowledge and a network of peers that I hope to collaborate with in the future.
This is part of a series of posts by recipients of the 2024 Career Services Summer Funding Grant. We’ve asked funding recipients to reflect on their summer experiences and talk about the industries in which they spent their summer. You can read the entire series here
