That's fine, but you express yourself in a way that sounds like you have a deep understanding of LL, and its relationship to other subjects such as programming languages and economic games. You have gotten a lot of pushback here for this reason, I'm just expressing myself more bluntly than other. Sorry, but you don't currently have this knowledge, and that might be misleading to others. I recommend to take this criticism constructively, and deepen your knowledge of logic (linear or otherwise), and there is only one way of doing this, which is to go beyond intuition and informality, and "do the math".
How many people do you think are familiar with it?
A lot on HN. Including myself, having written several papers on the subject, and discussed LL on numerous occasions with the world's leading researchers in the area, including Girard himself and several of his students.
HOTT states nothing about optimization.
None of the foundations of mathematics
really tackle optimization.
This is a complete misunderstanding of the foundations of mathematics. ZF(C) doesn't mention the natural and real numbers either. You can construct the rational and the real numbers in all foundations of mathematics
(and this is typically done in undergraduate maths see e.g. [1] where I learned the construction from).
Notions of minimun/maximum as well as related concepts can be expressed, too. This means that all mathematical optimisation as conventionally understood is trivially expressible in e.g. ZFC.
There is such a thing as linear types
I know, I coauthored some of the early papers on linear types.
Linear types let you to trully distinguish
between values and references.
No, linear types let you distinguish between values that are guaranteed to be used exactly once, and values that may not be used exactly once. Note that Rust (at least last time I looked -- the language evolves fast) has more like affine rather than linear types (guaranteeing use at most once).
that our current understanding of math is really
"all there is".
Nobody says this, indeed this is an immediate consequence of Goedel's incompleteness results.
[1] Yiannis Moschovakis, Notes on Set Theory (https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Math...)