The thing is that declarative contracts separate execution from verification. You don't actually execute the contract in the miner/verifier. The client executes the contract and records a trace of the subset of the program necessary to verify execution. The miner/verifier just uses the trace to verify that the presented state is correct (top-level contract rule evaluates to true).
In the simple and common cases, there ends up being no difference between execution and verification. However, if you have a contract that has
let F = (A() || B() || C() || D()) && ! E();
let R = F() && (G() || H());
R();
with an imperative contract that gets executed on the verifier, you need to optimally order the clauses A-D, taking into account the cost of each and the percentage of the transactions in which each one is true. The client isn't allowed to re-order the clauses in the contract. With a declarative contract that is executed client-side, the client tells the verifier exactly which one of the terms A-D needs to be evaluated and which of the terms G-H needs to be evaluated. Let's say G and D are the lowest cost functions that need to be evaluated to verify our transaction. If the execution trace is the child index taken in depth-first traversal of the tree of logical disjunctions in the contract expression then the trace indicating that D and G need to be evaluated is [3, 0]. This can be compactly represented as a single (potentially large) integer in a mixed-base number system. (In our case, the bases are 4 and then 2, so the single integer representing the trace is 2*0 + 3 = 3. The verifier first hits a 4-way disjunction, and 3 mod 4 is 3, so it only evaluates the 4th branch. 3 div 4 is 0. It next hits a 2-way disjunction and 0 mod 2 is 0, so it only evaluates the 1st branch.) If you order the logical disjunctions in your contract so that in the common case, the leftmost alternative is always taken, then in the common case, your execution trace as a mixed base integer is 0. With estimates of the probabilities of the branches, you could use an asymmetric mixed base number system, similar to Facebook's zstd compression to optimally represent your verification traces.
With a declarative contract, the cost of suboptimal ordering is borne by the client and not by the verifier.
With EVM, there's no separation of contract execution and verification. The verifier/miner needs to execute the contract at the request of the client. If you modify the EVM and contracts to keep track of what's provably side-effect free and allow the client to specify reordering of those terms, then you've by definition created a non-imperative language or sublanguage. In that case, it's much safer and easier to design the system from the ground up to have semantics that are invariant under evaluation order (that is, declarative semantics).
Most of the cost of declarative program optimization vs. imperative program optimization (deciding an optimal order) is borne on the client side. Due to the structure of the contracts and the traces, it's trivial to prove that portions of the contract don't need to be executed in order to verify the transaction.