Not sure what exactly you mean by "necessary", but I feel like the entire field of mathematics would disagree. Proving statements about infinite domains has a very long tradition.
The notion of a proof and verification of a real-life software are almost completely disjoint.
Of course, if you are interesting in proving statement about abstractly defined constructs: infinity is no issue as your domain is uniform. In real-life, this is not the case.
