Articulating the ineffable. Programming language theory 
cognitive psychology. PhD @Stanford
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
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 …
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
I recommend looking at Metamath, as it's *vastly* simpler than the others to build your own.
Subscribing/bookmarking this thread 
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
