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
Not sure if it's what you're looking for, but here's a pretty good tutorial for implementing a dependently typed language https://www.andres-loeh.de/LambdaPi/
Yes, I'd also like to know how much implementing a dependently-typed language would answer my questions. (I have a copy of The Little Typer that I keep meaning to revisit...) The relationship between dependent types <-> theorem proving is still not 100% clear to me.
Curry-Howard correspondence! :) I would recommend Wadler’s Types as Propositions for this, only because there is no other better paper.
I understand Curry-Howard in the abstract, but it doesn't seem to be the full picture. e.g. CHC is usually explained as correspondences between functional programs and constructive logic, incl. warnings against excluded middle. But in Lean, I can just call "classical.em". Why?
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
