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.
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”.