You are not really learning how to make proofs though, you are learning how to make specifications. There is an important difference. It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you. It comes down to the fundamental concept of computability. You won't learn true proving if you don't at least attempt to work through e.g. Cantor or Epsilon-Deltas.