Kind of embarrassing, but I cannot! The thing is, development of mechanised theorem proving has been driven by computer scientists, so proving program correctne

Kind of embarrassing, but I cannot! The thing is, development of mechanised theorem proving has been driven by computer scientists, so proving program correctness, doing programming language semantics, and explaining constructive ideology is at the heart of most introductory text books. I would recommend just following the "Theorem Proving in Lean" book for starters.