Two computer science bachelor students - Felix and Kasper - have developed a new tool to help their fellow students to better navigate one of the programme’s courses: Computability and Logic. The tool, called Logicbox, aims to make it easier for students to write, test and understand formal proofs, without requiring a lot of coding from the students.
Computability and Logic is a second-semester course that introduces students to the foundations of theoretical computer science, including questions about what can and cannot be solved by algorithmic methods. As part of the course, students work with formal proofs and proofs systems.
Current sixth semester students Felix Berg Pedersen and Kasper Skov Hansen were introduced to an existing proof-checking program, when they took the course on their second semester.
“The existing program worked well but needed us students to write a lot of code, I felt that I had to be careful not to make errors. So, after the semester ended, I wanted to try making my own proof checker, something that was easier for students to get started with,” Felix says. His first version ran entirely in a terminal with a lot of white text. “It worked, but it wasn’t exactly beginner friendly.”
Kasper noticed the project on Felix’s laptop. With experience in both front-end and backend development, he immediately saw an opportunity to improve the tool.
“My first thought was that he needs a frontend for that,” Kasper says. Felix agreed, and the two teamed up to transform the early prototype into something more accessible.
Over the following months, the pair developed Logicbox. To make sure it was user-friendly, they tested it continuously on fellow students at the weekly Friday bar.
“It was the perfect place to get honest feedback,” Felix says. “Seeing students interact with it gave us a really good sense of what worked and what didn’t.”
As Logicbox began to take its final shape, they realized that it could be a useful tool for students. They set a deadline for themselves and arranged a meeting with Professor Jaco van de Pol after the summer holidays to present their work. The meeting became a key milestone. “Jaco asked a lot of good questions, so we wanted to show him something solid,” Felix and Kasper explain.
“Logicbox looked nice from the beginning, but it was only able to solve easy logic proofs. So, I pushed them and asked them to develop it further,” says Jaco.
By the next meeting Logicbox could solve the complicated logic proofs as well.
“That was impressive.” Says Professor Jaco van de Pol
Since the fall, Logicbox has made its way into the Computability and Logic classes. Assistant Professor Daniel Gratzer says “Logicbox is more interactive compared to the old tool, the students not only use it to check their proofs, but also to learn the logic behind the proofs. So, it’s a more versatile tool for learning.”
Alongside his studies Felix works as a teaching assistant for the current second-semester computer science students and Logicbox is now a part of his teaching practice as well.
“It’s a little surreal to use something we built ourselves when we teach,” Felix says. “But it’s also incredibly rewarding to see students benefit from it.”
Kasper is teaching assistant on courses related to the fourth semester, where Logicbox has inspired one student to start developing a competing version. “We may have created a friendly bit of competition” Kasper says with a smile.
Felix and Kasper are now in their sixth semester and working on their bachelor's theses. Felix’s project is closely related to Logicbox, exploring topics inspired by the development process. Kasper’s thesis focuses on zero-knowledge proofs and includes developing a prototype for a secure e-wallet - a technology expected to become increasingly important in the EU’s digital strategy.
After the summer, both plan to continue their studies, where they will begin their master’s degree in computer science.
