Interactive Theorem Prover
Have you ever wished for an easy way to check your proof with Hoare logic? Or effortlessly review countless proofs sent in by students? Then the Interactive Theorem Prover is just the tool you need! With this online web application, you can check the correctness of a proof with just a few clicks. Simply type or paste your proof into the text editor and click on the check button. Done.
The Interactive Theorem Prover is carefully developed with perfection in mind. We wrote more than a hundred tests to make sure the checker is flawless and catches every possible error. We also poured a lot of attention into the design of the web application to create a smooth user experience on every major browser. That way we can guarantee that the Interactive Theorem Prover is a simple as well as a highly effective tool for you to use.
When you check your proof, the application will give instant feedback. If it's completely correct, it will say so. If there is an error, it will indicate what the error is and, if possible, on which line and column. The position of the error is given in both textual form as well as visual cues. On top of that, a KaTeX version of the proof is rendered. This all means you can immediately pinpoint where the error in the proof is.
What's more, when a Hoare logic rule is broken, the program will direct you to the corresponding section on the about page. There, it explains the rule so you can immediately understand what you did wrong and learn from it. This makes the Interactive Theorem Prover also a perfect tool to teach basic Hoare logic to students and let them practice the process of creating proofs.
Finally, we have integrated different levels of strictness into the checker: strict, equivalent assertions allowed, and missing assertions allowed. Depending on which level is chosen, the program will or will not allow for certain (more trivial) parts of the proof to be skipped. This leads to more flexibility and allows you to choose which part of the proof you want to focus on.
All in all, the Interactive Theorem Prover is an excellent tool to teach as well as study Hoare logic and proof writing. It guarantees accurate and clear feedback together with a slick design to deliver the best possible user experience. Are you ready to boost your productivity now? Come visit https://interactive-theorem-prover.herokuapp.com/!
Our client is Hans-Dieter A. Hiep, a PhD student and teacher at the faculty of Science of Leiden University. He wants to use the Interactive Theorem Prover as a tool for the subject Program Correctness. Primarily for himself to use while explaining, but also for the students to check their own proofs. For this purpose, he gave us one absolute goal: create a working and flawless checker.
Our collaboration with Drs. Hiep went very smoothly. We kept in touch regularly through emails and meetings to discuss problems and show demos. He was very clear in his wishes and priorities for the project. This made it easy for us to focus on the most important aspects. He was very satisfied every time we showed him our progress, and we, too, were very happy to work together with him.
Our team consisted of members with various backgrounds. This gave us a wide range of skill sets that all proved to be valuable throughout the whole project. Not only did we know many different technologies, but we also had diverse soft skills that were essential to the process.
The teamwork was very smooth and positive. We striked a perfect balance between building good relationships with each other and working on the project. Though there may have been some minor issues, we were able to communicate well with each other to solve it efficiently. This all led to a very fun and motivated experience throughout the whole development of the Interactive Theorem Prover.
We worked hard to bring life into this project. And we are all very proud of what we have achieved after many weeks. It is therefore our sincerest wish that the Interactive Theorem Prover can truly make a difference for the client and the students that will use it.