Talia Ringer on Nostr: Tarski actually has a lot of appeal as a kernel too IMO (really small axiom set, ...

Tarski actually has a lot of appeal as a kernel too IMO (really small axiom set, decidable proof search) but students felt the axiom set was so, so low-level that it was too hard to build the infrastructure needed to have good usability on top of that