Are there any good resources for building your own proof assistant? I don't really get Coq vs. Lean vs. F* vs. Idris, but I feel like I would get it more from building a pedagogical implementation. e.g. Mini-Pyro was really useful for understanding PPLs: https://pyro.ai/examples/minipyro.html …
Nothing's off the table! But I'd like to start with whatever logics are most commonly used for proof assistants.
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
cognitive psychology. PhD