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.
alt Hacker News
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/