2020-11-23 5:26:46 (GMT)
Intriguing, no? https://practal.com/ :smile:
2020-11-23 10:30:54 (GMT)
It certainly is, who is behind it?
2020-11-23 10:36:58 (GMT)
John Harrison (https://www.cl.cam.ac.uk/~jrh13/) i.e. Mr. HOL Light
2020-11-23 10:51:36 (GMT)
How did come to that conclusion? I thought it was Steven Obua (at least he's claimed to be the author of practal on the CICM slack).
2020-11-23 10:52:38 (GMT)
I guess by clicking the link at the bottom of the page. The page certainly looks more Obuaesque than Harrisonish.
2020-11-23 10:58:4 (GMT)
sorry -- yeah; should have realized that the link is just a reference.
2020-11-23 15:39:27 (GMT)
As a perfect Philistine, what is the difference between Tarski Grothendieck, and ZF? Would it impact the actual use of the ITP, or just the way foundations are built?