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?
It might be a little late, but perhaps it could help for someone else watching this question. I'm currently studying Intuitionistic Logic from the second chapter in the the book "Lectures on the Curry-Howard Isomorphism" (1998 version): https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf It seems like it fits your description.