>>14349237They directly limit computational power by limiting and controlling duplication of premises (data) and, in more limited linear logics like EAL, how complex a recursion may be performed.
Normal linear logic has the same expressivity and strength as constructive and classical logic, but it keeps (some of) the advantages of controlling data duplication. In that way, it has a similar relationship to them, as constructive logic has wrt classical.
If constructive logic demystifies and gains control of what LEM does in classical logic, then linear logic does the same to constructive logic, and locks all the "infinitistic" stuff derived from logical contraction behind two logical modalities, making the infinitistic assumptions explicit and manipulatable.
Limited linear logics like EAL, limit more explicitly the complexity class of the functions they can express, by controlling not only the duplication of data, but also by limiting the origin of the data upon which recursion may occur. This is done by having recursively generated data be locked behind a logical modality, out of which they cannot get out. It's a very ultrafinitistic idea.
They probably could be extended to have the same expressive power as normal linear logic by locking the extra power behind yet another modality, but as far as I know that has not been done.
As you may or should know, all of the above cannot be Turing-complete (although it can be safely locked behind a monad, like IO in haskell), as Turing-completeness usually entails that the corresponding logical systems derives a contradiction.
What's also interesting is that linear logic is also inconsistency-resistant (paraconsistent): it lacks explosion, so only truly "explosive contradictions", contradictions that entail everything by their nature, are explosive. But that's not really related to finitism, although it may be interesting for programmers.