I do mention that one should probably work with a LISP variant at some point, at a bare minimum. Being able to think in functional programming ways is definitely important, especially when you start dealing with things which blur the lines between math notation and programming language.
On PL theory and functional programming beyond the basics of LISP (and also the related topic of compilers), I mostly think the existing tools/theory just aren’t that great and will likely look quite different in the future. That said, it’s an area which goes a lot deeper than my knowledge, and my belief on the matter is weakly-held.
I do mention that one should probably work with a LISP variant at some point, at a bare minimum. Being able to think in functional programming ways is definitely important
There’s functional programming, and then there’s functional programming. The term is overloaded almost to the point of uselessness: it mostly just means not-imperative. But beyond that, lisps have little in common with MLs.
Lisp is python done right, and is best suited for the same sorts of domains: those where inputs are messy and everyone is ok with that, runtime errors are easy to surface and cheap to fix, and mostly-right means mostly-as-good.
MLs are theorem provers done wrong done right, and lend themselves to a pretty much orthogonal set of problems: inputs are either well-structured or dangerous enough that they need to have a structure imposed on them, runtime errors can be subtle and/or extremely bad, and mostly-right means wrong.
And, you mentioned proof and how it’s disappointing that analysis is fodder for proofs, which I roughly agree with and roughly disagree with (analysis is nice because you can review and strengthen calculus while leveling up in logic. Parallelization!)--- I’d like to nominate logical foundations. It gave me a very thorough foundation after a couple years of community college, it’s the kind of learning that you feel in your bones if you do it interactively. Executable textbooks in general are, I think, more bang for buck than classical textbooks.
Love this! You’re really mild on programming language theory and functional programming. Any comments on the omission?
I do mention that one should probably work with a LISP variant at some point, at a bare minimum. Being able to think in functional programming ways is definitely important, especially when you start dealing with things which blur the lines between math notation and programming language.
On PL theory and functional programming beyond the basics of LISP (and also the related topic of compilers), I mostly think the existing tools/theory just aren’t that great and will likely look quite different in the future. That said, it’s an area which goes a lot deeper than my knowledge, and my belief on the matter is weakly-held.
There’s functional programming, and then there’s functional programming. The term is overloaded almost to the point of uselessness: it mostly just means not-imperative. But beyond that, lisps have little in common with MLs.
Lisp is python done right, and is best suited for the same sorts of domains: those where inputs are messy and everyone is ok with that, runtime errors are easy to surface and cheap to fix, and mostly-right means mostly-as-good.
MLs are theorem provers done wrong done right, and lend themselves to a pretty much orthogonal set of problems: inputs are either well-structured or dangerous enough that they need to have a structure imposed on them, runtime errors can be subtle and/or extremely bad, and mostly-right means wrong.
I agree that tooling based on curry howard correspondences isn’t great. We live in a somewhat primitive time. Maybe you’re interested in my brief speculation about formal verification as a sort of dark horse in alignment, I look at FV and the developer ecosystem question which lags behind the state of the art theory question.
And, you mentioned proof and how it’s disappointing that analysis is fodder for proofs, which I roughly agree with and roughly disagree with (analysis is nice because you can review and strengthen calculus while leveling up in logic. Parallelization!)--- I’d like to nominate logical foundations. It gave me a very thorough foundation after a couple years of community college, it’s the kind of learning that you feel in your bones if you do it interactively. Executable textbooks in general are, I think, more bang for buck than classical textbooks.
Meta edit: hyperlink isn’t working, softwarefoundations.cis.upenn.edu/ maybe this is better.
oh haha two years later it’s funny that 2 years ago quinn thought LF was a “very thorough foundation”.