Hacker News Reader

Comment by mrkeen | Hacker News Reader

> Take it further down the stack and see that functional semantics are always executed by imperative machines

And the other way around too. Even your C compiler can't reason about mutability, so it un-imperatives everything first:

  int foo(int i, int j) {
    while (i < 10) {
      j += i;
      i++;
    }
    return j;
  }

That (j += i) line becomes:

  %9 = load i32, ptr %3, align 4, !dbg !23                  // read i into %9
  %10 = load i32, ptr %4, align 4, !dbg !25                 // read j into %10
  %11 = add nsw i32 %10, %9, !dbg !25                       // sum %9 and %10 into %11

(i++;) becomes:

  %12 = load i32, ptr %3, align 4, !dbg !26           // read i into %12
  %13 = add nsw i32 %12, 1, !dbg !26                  // store i+1 into %13

View on HN

I'll admit to not being super great at getting down into the nitty gritty with internals of compilers. Are you talking about some sort of IR? Because if we're talking about the output, mutation definitely happens.

Checking on godbolt, there's definitely mutation at least sometimes. Using gcc 13.2, I get the following output.

j += i; becomes:

    movl    -4(%rbp), %eax     // move i into %eax
    addl    %eax, -8(%rbp)     // add i to j

With i++ becoming:

    addl    $1, -4(%rbp).      // add 1 to i

If your example is IR, do you happen to know how it crunches everything "back down" to mutability? Does it just check that the previous value of i and j were never used and use the same registers as an optimization?

I would consider the compiler to be working in the functional realm, for most of its ideas. Such that I would think it is between the imperative of the machine and the imperative of what a person is thinking?

That said, I confess I'm curious how on what the constraints are on this one. I thought there was an increment instruction, specifically. I'm guessing safety and general debugging concerns? And it occurs to me that you are showing an intermediate language in this? Static Single-Assignment (SSA) is definitely in the vein of moving imperative to functional for easy manipulation there.

Definitely fun topics to explore here.

I've come to the conclusion that executability and reasoning are separate axes. If we view everything in terms of languages with interpreters, of course functional semantics must be executed by imperative machines. But to reason about either kind of program, we need functional semantics, because functional programming is the language of pure reasoning.

More on the subject: https://concerningquality.com/quality-and-paradigm/

But folks have reasoned about imperative things for a long time, as well? It is certainly easier for many analytics to get into a functional form. But would be a stretch to say it is always easier. Fractals are often my go to example where imperative is easier for many constructs.

I view it like coordinate systems. Polar versus Cartesian coordinates can clearly both do the same things. They each have domains where they have advantages.

You could argue that time based logic systems are the end goal, maybe? Still feels like throwing babies in bathwater.

Edit: for a fun example of reasoning without programming "functional" logic, look up juggling diagrams/notation. Not all logic is symbolic in the same way.

This doesn't feel in contrast to what I was saying. You can reason about imperative code, but you have to add things to it to reason about it, most importantly the notion of a memory store. This is because imperative code assumes an underlying CPU + RAM which holds state.

It's not that it's easier, it's that imperative code has implicit state.

Fair that I don't intend my question there as a full rebuttal. I do question if functional semantics are fully needed any more so than other tools. In particular, I recall formal methods was more about prepositional logic than it was functional semantics.

And yes, you have to add and remove things to any model to really be able to reason about it. Is why engineering dynamics is harder than engineering statics. Things that change are hard. Reducing this to state being the enemy, though, I think is wrong in a lot of functional advocacy. State can be reasoned about without having to boil the ocean, as it were.

Reply on news.ycombinator.com