in agda, I think ctrl-c ctrl-a is the "I feel lucky" button. Plfa is definitely good, Connor Mcbride is pretty good too https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37ox...

and yes programming with holes is almost magical. I really like "run as much as you can" then complain when you get stuck. kind of a mind blowing change for me.