Proof assistants allow to state that
$$A(BC) = (AB)C$$
with $A$,$B$,$C$ compatible matrices,
Is there a formal system that takes this sort of equations to choose among interpretation strategies of some target language, say for evaluation, the one with the lowest cost?
I would say that this paper, with code in Coq, meets your requirement: Verified tensor-program optimization via high-level scheduling rewrites
First two sentences of the abstract
We present a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites.
You can find the code on GitHub.
Edit: Reading the question again. This does not prove the rewritten program is faster, only that it computes the same result as the original. So it might not be an answer to your question.
I think your question can be interpreted in many different ways. Since you tagged it with coq, lean, and agda (initially), I assume you are interested in dependent type theory. DTT is special in that it is a language for both mathematics and computation, and therefore it can be used to build proof assistants (Coq, Lean 3/4, Agda) and fully functional programming languages (Lean 4, Idris, Adga).
Now, if we consider DTT from the point of view of a programming language, there are even two places where code is "run". The first is internally in the proof assistant. If you prove 1 + 1 = 2, one way to do this in the CiC implementations of DTT is by reducing both sides to the same thing. In Lean for example, this is the rfl term or the refl tactic. In Coq, it is the reflexivity tactic. One doesn't even need to have closed terms. x : nat |- 1 + x = S x is provable by reflexivity in Coq since 1 + x = S x by definition. Also, it is the same mechanism which lets you type-check something like x : Fin (1 + 1), y : Fin 2 |- x = y since for x = y to type check, their types must be the same and that means 1 + 1 must be definitionally equal to 2.
My understanding is that evaluation in the reflexivity tactics at least naively reduce the term in a deterministic way, unraveling the definitions. So when evaluating 1 + (2 + 3), there is some freedom of evaluating (1 + 2) first or unraveling 1 + (...) to S (...) first (and I don't know the details to know how it is done in practice). But one can't change the term to say (1 + 2) + 3 in the computation.
I'm brushing something under the rug here also about numbers, but it is worth mentioning since you care about fast code. In a proof assistant when you write 3, that is syntatic sugar for either a (DTT representation of) the unary SSS0, the binary 11 or the decimal 3 depending on the proof assistant and some settings. Working with the latter two can make arithmetic faster.)
Now this reflexivity code is run in the "kernel" and it is possible to optimize the kernel. For example, Coq's kernel is more optimized than Lean's (especially Lean 3's) letting it run much more intense computations. One could even go so far as to optimize standard math operations by implementing say 1 + (2 + 3) on the chip using standard big ints instead of by using the base definitions of +. However, every optimization comes with a cost to the assurance that your kernel is correct. A bug in a kernel could make it impossible to prove some stuff, or worse possible to prove a contradiction.
Now, keeping with computation in proofs, it is possible of course to redefine any operation to be faster. So for example, the naive definition of the Fibonacci numbers is slow in any programming language. But you could optimize the computation. However, base DTT and its common axiomatic extensions like classical logic and univalent foundations, are compatible with functional extensionality. Therefore, all implementations of fib would be equivalent from the point view of what you can prove about them in the logic. In particular, you could couldn't prove that a dynamic programming implementation of fib is faster than the naive version. You could only define fib and fast_fib and prove they are equal (or equivalent if you don't have FE) functions. Then to prove fib 20 = 6765 you could first rewrite fib to fast_fib and then do reflexivity.
To avoid having to manually rewrite all functions with their faster versions, there are other tricks where instead of using the built in reflexivity tactic, you use a tactic which evaluates your expression for you in an efficient manner. In Lean 3, there is norm_num which applies rewrite rules which evaluate expressions in arithmetic in a binary way instead of a unary representation. It is much faster than Lean's built in refl. As such, one could certainly have a norm_num-like tactic for other computations like matrix arithmetic.
In Lean and Agda, it is possible to run code directly as if these were programming languages. I believe Lean 4 and Agda are both especially designed as a user-friendly functional programming language to say rival Haskell. Now, again if you make a definition fib, the VM or compiler will run the code you wrote mostly as written. However, there are a few more possibilities for optimizations. I'll just talk about Lean 4 since that is what I know. Lean 4 lets you replace any definition with another for the purpose of computation. This doesn't effect the logic, so you can't prove false, but it still would allow you to get into trouble if you don't replace the pure Lean function with equivalent functionality. (This often happens around edge cases like 0.)
There are a few ways to do this in Lean 4. For one, Lean 4 has a foreign function interface which lets you say replace a particular Lean function with a C version. I know all of Nat arithmetic in Lean 4 is compiled to fast integer libraries. Similarly, you can replace a Lean function with another faster Lean function and I think (but I can't find the reference in the manual at the moment) that you also have the option to prove that this faster Lean function is equivalent to your original, increasing the trust of your compiled code. (Lean 4 is filled also with a number of other optimizations such as in place memory usage and pointer equality checking, which are possible since the programming language is so pure.)
Finally, many ITPs including Isabelle/HOL as well as DTT ones offer different ways to talk about and extract code. For example, CompCert was a verified C compiler verified in Coq. I'm not really familiar with this, but this would likely give you methods of being able to talk about code run-time without violating function extensionality and also let you extract this code to other programming languages like C or OCaml. But again, I don't know much about this.
