This is getting it backwards. The first introduction to CS is precisely when proofs matter most. I agree that, ultimately, not everything has to be proven corr

This is getting it backwards. The first introduction to CS is precisely when proofs matter most. I agree that, ultimately, not everything has to be proven correct. Often there isn't even a well defined criterion for software correctness. But proofs absolutely matter in certain domains (algorithms, databases, compilers, etc.), and there's no way you can be ready to prove things about moderately tricky programs if you don't have practice proving things about toy ones.