Wadler's Blog

I've played with Coq and become pretty comfortable with it. But I also had trouble with ProofWeb. I had to look at the documentation to see what the tactics meant (they are lower-level than Coq's standard tactics). It wasn't too bad once I got the hang of it though.