The thing that blew my mind was that there are some mathematical programming languages where the point is not to ever actually run the program. Just type-checking it is enough to prove the result. (In the "programs are proofs" sense.) In these languages, it's important not to allow infinite loops because you will never test the code.

Even though there's a correspondence, there's always going to be a difference between writing a program so that you can actually run it and writing proofs, where you don't, and ridiculously inefficient algorithms don't matter at all, so long as they don't diverge.