Although I had absolute no idea what I was doing when we played around with Agda in university, it was kind of fun constructing a few very basic proofs. It kind of felt like smashing some buttons until it worked. The Emacs integration with all the Unicode goodness was really something.