> Are we still talking about models other than functional here? Because I'm surprised to hear you say that if so.

TBH, I didn't understand your question, so I may have written something irrelevant. In any event, the functional denotation does not distinguish between two different algorithms for computing the same function, and cannot relate different expressions of the same algorithm (or none). This is not necessarily a disadvantage, but rather a conscious choice with various tradeoffs. But this choice has implications both on the ability to analyze and compose programs, especially when they're not sequential.

> whatever your example was supposed to show, you didn't actually use the monadicity of the state monad at all

Let me try again. Hopefully, these examples will make my point clearer. Consider:

    fac5 :: Int -> IO ()
    fac5 0 = writeFile "fac.txt" "1"
    fac5 n = do
        fac5 (n - 1)
        f' <- readFile "fac.txt"
        evaluate (force f') -- WTF
        writeFile "fac.txt" $ show (n * (read f' :: Int))

    fac6 :: Int -> State Int ()
    fac6 0 = put 1
    fac6 n = do
        fac6 (n - 1)
        f' <- get
        put $ n * f'

There is simply no way to relate fac5 and fac6 to fac1 or fac2, even though they're the same computation. A lambda expression is opaque; you can't extract its internal operation to transform it into an "imperative" monad (the problem isn't that the expression is opaque, although making it transparent, as Lisp does, is one way of adding more power to languages based on LC; formalisms that don't use functional denotations allow for more powerful composition and an easier way to compare and relate algorithms while still having opaque expressions, but ones that don't represent functions).

There is a way to relate fac5 and fac6, but that requires rewriting them and extracting some common monad (maybe the free monad?) that will give them both the same denotation. (This, BTW, is another problem with functional formalisms. For example, in TLA+ (or even in Java, as you’ll see below), you just write your algorithm and then prove whatever it is that you want, and if your proposition is provable, this can always be done, by some completion theorems. However, in Lean, or let alone in Idris, you have to write your program with what you want to prove about it in mind. Oh, you also want to state a proposition about complexity? You have to rewrite the program with types that express complexity.)

Now, let's see how this can be done in formalisms with other denotations. Let's look at classical imperative programs, but first we need to understand what the denotation is (unfortunately, even people who are interested in the mathematics of programming often learn the mathematics of functional programs and not that of imperative ones). In imperative classical programs, the denotation of every statement is a transformation on state. It is not necessarily a function, as some statements are nondeterministic from the perspective of the static program, like generating a random number or reading input, which put the following state in one of many possible ones. Mathematically, there are two ways to describe this. We can view each statement as a relation on the previous state and the next one (the state machine denotation), or as the set of all propositions that are true in the preceding and following state (the Hoare triplet denotation). For our purposes, both are equally fine, but in my example it may be easier to consider the Hoare logic one, as I won’t be representing the relation formally.

How do we express this denotation formally? Well, as my example is in Java, I could use JML, a formal specification language embedded in Java programs, which, among other things allows you to create “ghost” variables and functions (those are variables that are not necessary for the computation, but are used to state things formally about the denotation) that are then removed from the program. But, to make things simpler (and I assume you don’t know JML), we’ll note that ordinary assertions do exactly that. They express a proposition that is either among the true ones or the false ones for that state. I’ll mark my ghost variables and functions in comments (unlike the Haskell programs, which I tested because I don’t really know Haskell, I didn’t test the Java ones, so forgive me if I’ve made some mistakes):

    class Factorial {
        // reasoning helpers:

        int N; // ghost
    
        int factorial(int n) { return n == 0 ? 1 : n * factorial(n - 1); } // oracle
    
        long stackDepth(String name) {// the number of consecutive frames of the given method in the call stack
            return StackWalker.getInstance().walk(stack -> 
                    stack.dropWhile(f -> !f.getMethodName().equals(name))
                          .takeWhile(f -> f.getMethodName().equals(name))
                          .count());
        }

        // programs:
        
        void fac1(int n) { N = n; /* ghost */  _fac1(n); }
        
        int _fac1(int k) {
            int f;
            if (k == 0)
                f = 1;
            else
                f = k * _fac1(k - 1);
            
            // denotational specification
            long n = k + stackDepth("_fac1") - 1; // ghost
            assert( f == factorial(k) && n == N );
            
            return f;
        }
        
        int fac2(int n) {
            N = n; // ghost
            int f = 1;
            for (int k = 1; k <= n; k++) {
                f = f * k;
                
                // denotational specification
                assert( f == factorial(k) && n == N );
            }
            return f;
        }
        
        void fac5(int n) { N = n; /* ghost */  _fac5(n); }
        
        void _fac5(int k) {
            // assuming appropriate methods, writeFile and readFile

            if (k == 0)
                writeFile("fac.txt", 1);
            else {
                _fac5(k - 1);
                writeFile("fac.txt", k * readFile("fac.txt"));
            }
            
            // denotational specification
            int f = readFile("fac.txt"); // ghost
            long n = k + stackDepth("_fac5") - 1; // ghost
            assert( f == factorial(k) && n == N );
        }

        void fac6(int n) { N = n; /* ghost */  _fac6(n); }

        int F;
        void _fac6(int k) {
            if (k == 0)
                F = 1;
            else {
                _fac6(k - 1);
                F = k * F;
            }
    
            // denotational specification
            int f = F; // ghost
            long n = k + stackDepth("_fac6") - 1; // ghost
            assert (f == factorial(k) && n == N);
        }
    }

As you can see, while the programs are very different from one another, the denotation of all is isomorphic, as is easily shown.