If you perform the echo without the (int) cast, it resulits in:
echo ((0.1 + 0.7) * 10); 8 So what happens is that the floating point actually represents it as 7.99999....
When you perform an (int) cast, the default behavior is to take the integral part, so that's 7. Although it is extremely close to 8, it is not the behavior of a cast to round off.
The errors are due to the fact that floating point numbers are represented with a binary radix. Representing 0.8 correctly is thus impossible. Floating points round off the answers, and hope it doesn't bother that much. When you represent the floating point like 0.8, the result is 0.80000...
Proof of concept using the PHP interactive shell (php -a):
$ php -a Interactive mode enabled php > echo number_format(((0.1 + 0.7) * 10),20)."\n"; 7.99999999999999911182 php > echo number_format(0.8,20); 0.80000000000000004441