Lately I've gotten a friend of mine interested in mathematics. He has no college-level education to speak of, but is well employed as a software engineer. So I feel he's competent to learn this stuff on his own.
He asked me recently if there was a 'mathematical' version of "The Little Schemer".
The point being, if there was an "introduction to proofs" book which took a more hand-holding approach. He's also expressed fondness for the metamath project.
However, metamath's proofs are obviously a bit too low level to learn anything serious.
At one point in our conversation, I mentioned the dependently typed programming language Agda, but I felt it's not quite as helpful until he at least gets some experience with Haskell (for which the target audience of Agda is Haskell programmers, hence the similarity in syntax).
Anyone have any good suggestions on a book?