Conversation

don’t know what this is but it sure looks beautiful

Quote Tweet

The next version of Holbert will include: Support for elimination rules, support for rewriting with equalities, a revamped goal interface, prose style proofs and now including dark mode!

Show this thread

Brendan Zabarauskas

@brendanzab

Feb 6

Alfa is another tool worth checking out! Lets you swap between different projections of a proof, including natural deduction: cth.altocumulus.org/~hallgren/Alfa

@kamatsu8

has brought this up in conversation with me in the past too:

Quote Tweet

Brendan Zabarauskas

@brendanzab

· Oct 19, 2020

Replying to @kamatsu8

Yeah Alfa is suuuper neat! I'm a big fan! cse.chalmers.se/~hallgren/Alfa/

Liam O'Connor

@kamatsu8

Feb 6

Alfa is great but it's still a type theory tool first and presentation tool second. Most PL/CS books that use a proof assistant spend >50% of the book talking about the mechanics of the tool. Holbert aims to bring that down as low as possible. With Alfa it would still be >50%.

Brendan Zabarauskas

@brendanzab

Feb 6

Nice, helpful to have that comparison!

Replying to

and

(I also find Alfa a bit clunky to use in practice, and Holbert seems to make improvements there, but that's separate to it being designed as a type theory first)

2:45 AM · Feb 6, 2022Twitter Web App

Replying to

and

To be fair, Holbert also doesn't take the structural editing to the term level, and editing rules is a little annoying in Holbert. The main thing I wanted, which Holbert does really well, is the "video game" feel of proving things.