That's a legitimate question. It's just floating-point jargon. Here's what it means:

> I’m well aware of banker’s rounding, and rounding up, and round down, and rounding towards zero, and rounding towards signed infinity, etc.

MPFR supports most of those rounding modes you mentioned:

https://www.mpfr.org/mpfr-current/mpfr.html#Rounding

> But “correct” as a formal modifier is new to me

It just means that once you select a rounding mode, it is guaranteed (modulo bugs) to give you the correct answer rounded according to your selected rounding mode.

At first one can think: "obviously, who wants incorrect rounding?". And indeed all recent floating-point hardware implements correct rounding... But only for 32- or 64-bit floats, and only for addition, subtraction, multiplication and division.

By contrast, most libc/libm implementations do not have correct rounding for transcendental functions (cos, sin, tan, exp, log, etc.). There are some exceptions (Rlibm, CRlibm).

MPFR implements correct rounding

- at any bit width and

- for all transcendental functions.

In a big application, wouldn't rounding to a random direction (a feature GNU MP supports) be the most accurate probabilistically? If you round up or down all your numbers and you perform a lot of arithmetic operations, you create a lot of bias.

Consider the logarithm. In almost any interval, rounding down will be more accurate than rounding up the majority of the time -- so random rounding will bias you away from an accurate result. Random rounding can be a good idea, but it's not always a good idea. Random rounding is an okay default, but having fine-grain control over rounding direction is vastly superior to always sticking to the default.

For another example, interval arithmetic is a really cool approach to keeping an eye on your accuracy. There, you want to round your upper bounds up, and round your lower bounds down.

Maybe, but having random "accurate" behavior in a program is generally worse than being incorrect all of the time.

Correct rounding means that if the function result has X bits, all those X bits should be the same as when computing the result with infinite precision and then rounding it using the specified rounding mode.

For the ordinary arithmetic operations, including for square root and for reciprocal square root, there are algorithms to do correct rounding without excessive computation. Because of that, the standard for floating-point arithmetic specifies that a conforming implementation must use correct rounding for those operations.

On the other hand, for transcedental functions, like exponential, logarithm, sine and so on, there is no general method to guarantee that the result will be correctly rounded without having to compute an unlimited number of result bits before being able to round correctly.

Because of the difficulty, many mathematical libraries and also all hardware implementations of transcedental functions round correctly many of the possible results, but not all of them.

Nevertheless, for each usual transcedental functions and for the numbers of bits used frequently, i.e. single-, double- and quadruple-precision, there are known algorithms to round correctly, which have usually been found by exhaustive searches for corner cases, when more result bits must be computed than for most other results.

Doesn't it mean that, when you compute - say - sin(123.45) then the resulting computed value is - of all the finite numbers of possible floating point values that the underlying MPFR representation can encode - the one that is closest to the true value of sin(123.45)?

That may not be what it does, but that's certainly what I'd expect "correct rounding" to do.

This is correct.

Imagine you get the result correct with infinite precision, and then round to the required precision in the specified way (round up, round down, round towards zero, round to nearest with ties to even, etc.). Correct rounding is equivalent to this. It is also reproducible, as there is only one possible correct result.

There is a similar concept which is supported experimentally by MPFR, which is faithful rounding. With faithful rounding, a number is rounded either to the closest value up or to the closest value down, but it is not necessarily the nearest of them. That is, if a and b are representable and no value between them is representable, and if a < x < b, then with faithful rounding x will be rounded to any of a or b. This can sometimes be faster, but is not reproducible any more.