As someone curious with formal proof systems, I am not sure it's a good idea to start from there if you still need to grasp elementary concepts. They are really technical stuff. It's like working on an advanced optimizing compiler when you still learning how to use a for loop.