I've been working on an interactive click-and-prove prover that is backed by dependently typed terms.[0] The Proof Machine only goes up to some Simply-Typed Lambda Calculus terms, whereas I have the logic sufficiently powerful to support recursion and reasoning about programs and equality.
I got stuck in a loop on 8 "Adding zero to the right", blindly following the tip below the box keeps looping induction introduction. Looping 9 times following the help tip, it eventually complains about an invalid proof state (kernel isn't general enough?). Where's the inductive hypothesis... doh the green box labeled IH on the left side. User error lol. But I feel that folks unfamiliar with proofs would struggle with it.
Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.
Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.
Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.
I've been working on an interactive click-and-prove prover that is backed by dependently typed terms.[0] The Proof Machine only goes up to some Simply-Typed Lambda Calculus terms, whereas I have the logic sufficiently powerful to support recursion and reasoning about programs and equality.
[0] https://touchproof.siraben.dev/
I got stuck in a loop on 8 "Adding zero to the right", blindly following the tip below the box keeps looping induction introduction. Looping 9 times following the help tip, it eventually complains about an invalid proof state (kernel isn't general enough?). Where's the inductive hypothesis... doh the green box labeled IH on the left side. User error lol. But I feel that folks unfamiliar with proofs would struggle with it.
Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.
Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.
Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.
1 reply →