Short version: What is a good shortish introduction to intuitionistic logic, accessible to a relative beginner in logic?

Long version: I'm revising the frequently used Teach Yourself Logic Study Guide which aims to give recommendations for good books and other resources for self-study on different areas of logic. (This, by the way, is aimed at readers with a background in philosophy or maths, not at e.g. computer scientists.)

The Guide needs a better introductory section on intuitionistic logic (aimed at someone who has e.g. done a standard course on classical first order logic, but doesn't yet know much logic). Ideal reading would have something about motivation, the BHK interpretation, leading to Kripke semantics, and something about a proof system (e.g. natural deduction), and some light metatheory. So we are talking about a first pass at the area, not a full book's worth! -- e.g. something along the lines of what van Dalen attempts in Ch. 5 of his Logic and Structure (but perhaps better!). If you are a student, what has worked well for you as a first intro to intuitionistic logic? If you are a logic instructor, what do you recommend to your students?