I watched most of the Bob Harper OPLSS videos of 2012 [1] recently.

It felt like I was learning something deep when I was watching, but when I looked back on it later, I couldn’t remember any tangible insights or applications :( A whole lot about equality and then finally how useful dependent types are.

Was wondering if anyone else had the same kind of experience?

1 - https://youtube.com/playlist?list=PL5FJyaC2WsVmiZHLVm7Z718vb...

I think I might be in a similar boat. I've an interest in Type Theory, but rarely get to really connect day to day work with the fun bits.

Interestingly I have never heard of Robert Harper, so I will be looking at those lectures with great interest.

Instead, I have Benjamin C. Pierce's fantastic "Types and Programming Languages" book (still working my way through it bit by bit), and I happened to get one of the most impactful talks of my life from Derek Dreyer: How to Give Talks that People Can Follow. I still use those 20 minutes of advice to this day.

I'm strangely excited to see both their names as authors on this article, and I believe that tells me a lot about what kind of passionate speaking I can expect from Robert Harper!

OPLSS is what education should be: everyone is there to teach and to learn, because it's voluntary and you don't get anything else such as a piece of parchment. What we call education is gross perversion of it.

Similar experience—I came across his HoTT lectures on YouTube and was absolutely blown away by how clear and concise his teaching was. Absolutely transformed my understanding of the subject in just the first lecture.

I don't have a degree but attended OPLSS last year and it was really fun! Worth attending :)