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 …
-
Show this thread
-
Also interested in: - What logics form the core of modern proof assistants? - How is verification done efficiently? e.g. how is SMT integrated? - What are the hard parts of building a real-world proof assistant? e.g. it's easy to make an STLC interpreter, but hard to make OCaml
2 replies 1 retweet 4 likesShow this thread
Replying to @wcrichton
I recommend looking at Metamath, as it's *vastly* simpler than the others to build your own.
1:32 PM - 5 Mar 2020
0 replies
0 retweets
1 like
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.