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 i

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=PL5FJyaC2WsVmiZHLVm7Z718vbHXUxLtHM https://youtube.com/playlist?list=PL5FJyaC2WsVmiZHLVm7Z718vb...