Mathematicians and computer scientists do prove theorems about floating point arithmetic! For example, the most widely-cited floating point reference contains no fewer than fifteen theorems about floating point:
http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.ht...
Or here's a presentation about representing functions with their Taylor expansions using floating point arithmetic, providing strong error bounds on the result of adding or multiplying two functions represented in this way:
http://perso.ens-lyon.fr/nathalie.revol/talks/ICIAM07.pdf
I agree that many proofs in computer science are harder than proofs in mathematics, because you can't deal with idealizations - you always have to think about the machine. But unlike empirical sciences, we have access to the design of the machine. We know what many of the axioms are. Formal reasoning is valid for a far larger part of computer science than for the natural sciences.
I'm not going to argue that proofs are a panacea for every situation. But I also don't categorically reject them in the domains where they can be usefully applied.