format_float() currently does not to any thousands grouping eg:

1234567.89

vs

1,234,567.89

https://github.com/moodle/moodle/blob/master/lib/moodlelib.php#L8782

There is no reason it can't its just doing it properly and supporting all the funky languages that sometimes do 4 digits, or 2 digits, or sometimes 3 and then 2. php doesn't support this out of the box but it should not be that crazy to implement and would improve the UX / readability of many large numbers across many places.

https://en.wikipedia.org/wiki/Decimal_separator#Digit_grouping