What does "correctness" mean? It's impossible to talk about correctness without specifying what you are intending to compute. Numerical algorithms frequently have correctness conditions specified in terms of a precision (e.g. compute a floating point approximation to f(x) to within 1eps), and any algorithm that doesn't meet that precision is incorrect with respect to that correctness condition, by definition.
So you can think of this paper as saying "suppose you have a correct multiplication and addition operation on the field of interest. Then this algorithm for multiplying matrices over that field, which is composed of a sequence of those multiply and add operations, computes the correct matrix product." That is a perfectly provable kind of fact, that as you say doesn't stop being the case if you switch computers or something.
But fpmul and fpadd on your computer doesn't satisfy the condition for this proof! Therefore it doesn't apply, except by rough analogy. Then, other people might be interested in a different kind of proof, of a fact more like: "given two matrices of floating point numbers and fpmul and fpadd operations that are within .5eps precision, this sequence of fpmul and fpadd operations provably computes the matrix product such that the eigenvalues of the product are within .5eps of the true values". (edit to add: you could then also prove that the implementations of fpmul and fpadd on your computer satisfy the first condition, or replace them with implementations that do). That is also a well-specified correctness condition, and it is a correctness condition that is not necessarily satisfied by replacing "multiply" and "add" in the first algorithm with "fpmul" and "fpadd". This is what it means for "correctness [to be] context dependent". It doesn't invalidate the first proof, it just means we are interested in a different correctness condition than the first proof proves.
(edit to format, and add: of course different conditions on precision are relevant to different applications. Maybe I need my matrix elements to be computed within some absolute error bound, but my friend needs them computed within a relative error bound. Or I need it to be able to work on subnormal numbers within a certain precision, but my friend only needs it to be precise for numbers between 1 and 2. Different algorithms may satisfy one condition but not the other.)
Thanks for this comment. I think I started in this comment section trying to say something like this, but said it in a bad way, and then got progressively more confused and less clear in my responses as the day went on.
This is much more clear than anything I would have been able to write.
So you can think of this paper as saying "suppose you have a correct multiplication and addition operation on the field of interest. Then this algorithm for multiplying matrices over that field, which is composed of a sequence of those multiply and add operations, computes the correct matrix product." That is a perfectly provable kind of fact, that as you say doesn't stop being the case if you switch computers or something.
But fpmul and fpadd on your computer doesn't satisfy the condition for this proof! Therefore it doesn't apply, except by rough analogy. Then, other people might be interested in a different kind of proof, of a fact more like: "given two matrices of floating point numbers and fpmul and fpadd operations that are within .5eps precision, this sequence of fpmul and fpadd operations provably computes the matrix product such that the eigenvalues of the product are within .5eps of the true values". (edit to add: you could then also prove that the implementations of fpmul and fpadd on your computer satisfy the first condition, or replace them with implementations that do). That is also a well-specified correctness condition, and it is a correctness condition that is not necessarily satisfied by replacing "multiply" and "add" in the first algorithm with "fpmul" and "fpadd". This is what it means for "correctness [to be] context dependent". It doesn't invalidate the first proof, it just means we are interested in a different correctness condition than the first proof proves.
(edit to format, and add: of course different conditions on precision are relevant to different applications. Maybe I need my matrix elements to be computed within some absolute error bound, but my friend needs them computed within a relative error bound. Or I need it to be able to work on subnormal numbers within a certain precision, but my friend only needs it to be precise for numbers between 1 and 2. Different algorithms may satisfy one condition but not the other.)