Another example:

<?php
$dt1=new DateTime("2000-01-01 00:00:00");
$dt2=new DateTime("2006-01-02 03:04:05.000251");
$interval = $dt1->diff($dt2);
var_dump($interval->format("%R%Y-%M-%D %H:%I:%S.%F"));
/* Output: string(25) "+06-00-01 03:04:05.000250" */

The floating-point inaccuracy you are describing is far below the millisecond-range. The fraction-issue you are pointing out here relates to a mismatch of 299 meters when you're calculating distances based on the speed of light… 
In GPS a timing-error of 0.0001 second results in a 0.8m offset, so for the timing error we're talking about here we have an offset of 8mm 

Is this really relevant?

I'd rather say we document that it might be possible that the last digit of the fraction might be off by one.

> The floating-point inaccuracy you are describing is far below the millisecond-range. The fraction-issue you are pointing out here relates to a mismatch of 299 meters when you're calculating distances based on the speed of light…
> In GPS a timing-error of 0.0001 second results in a 0.8m offset, so for the timing error we're talking about here we have an offset of 8mm 
> 
> Is this really relevant?

It is a different topic whether there is a bug or not and whether the bug is harmful or not. Of course you know.

In addition, this bug report also points out the asymmetry on the implementation of DateTime.

<?php
$dt1=new DateTime("2000-01-01 00:00:00");
$dt2=new DateTime("2006-01-02 03:04:05.000251");
$interval = $dt1->diff($dt2);
var_dump($interval->format("%R%Y-%M-%D %H:%I:%S.%F"));
/* Output: string(25) "+06-00-01 03:04:05.000250" */
$dt3 = $dt1->add($interval);
var_dump($dt3->format);
/* Output: string(26) "2006-01-02 03:04:05.000251" */

Datetime::format() can handle up to the last digit of microsecond. And its implementation is the same as the patch I wrote.

This asymmetry would cause confusion.

> I'd rather say we document that it might be possible that the last digit of the fraction might be off by one.

Of course there is no problem as long as it is documented.

However, even #74356 points out the lack of the documentation for this implementation, there is no response for a month.

I'm sorry, example code is incorrect. Fixed version:

<?php
$dt1=new DateTime("2000-01-01 00:00:00");
$dt2=new DateTime("2006-01-02 03:04:05.000251");
$interval = $dt1->diff($dt2);
var_dump($interval->format("%R%Y-%M-%D %H:%I:%S.%F"));
/* Output: string(25) "+06-00-01 03:04:05.000250" */
$dt3 = $dt1->add($interval);
var_dump($dt3->format("Y-m-d H:i:s.u"));
/* Output: string(26) "2006-01-02 03:04:05.000251" */

Yes, that was a bug, and the attached patch would have helped;
however, as of PHP 7.2.0 the microseconds are no longer stored as
doubles, but rather as integers, so this issue is resolved.