If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.

As far as the IO thing is concerned, one could use pure functions to construct a model of an imperative program. Then you just need something to run it... There is a sense in which this is exactly what is done in practice.

> If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.

Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.

Is it easier to write a fully-correct 10,000-line-long math proof, or a 10,000-line-long program? Again, I'm not sure that the math is actually easier.

Is it easier to write a formal prover for the math? Almost certainly. And maybe, with a formal prover, writing the correct math is easier...

> Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.

Don't compare them on the basis of familiarity. Making your programming language look mathy is not the point.

I'd offer a different comparison:

Reason about a 10,000-line-long math proof, or a 10,000-line-long math proof in which there are instructions to jump back-and-forth with your pencil, crossing out and updating previously-calculated values in-place.

The most common proofs are those that the compiler constructs while type checking. The compiled program is the proof witness. All compilers can be thought of as producing a proof-by-construction but they vary wildly in the propositions they can prove.

If this idea is new to you and you want to learn more, google "propositions as types" or "the curry howard correspondance".

You don't do a single proof of the entire 10k line program, you do proofs of the many small functions that make it up. If you can use each proof as an axiom going into proving the functions that use it, then each of them becomes easier to prove too. If I have a function that might sometimes mutate a variable off in another part of the program, that's just inherently harder to reason about that one that is idempotent and guaranteed to have no side effects.

Well, why would it be taken as a given that programming should mimic the hardware?

Pure functions are easier to reason about (there may be exceptions of course), that's why they're interesting.

This paper is not related to side-effects - it's related to "totality", meaning all programs terminate. This could also be interesting for side-effecting programs, but it's of course much harder to verify in this case.

Due to the halting problem's existance a total language can not be Turing complete, but many useful programs can be verified.

I didn't see anything in the paper that claims that pure functions should be "all the way down", and the paper is not about side effects anyway.

A slight tangent: there's also a related notion to termination, that allows you to describe event loops.

Basically it's about the loop making progress on every iteration, but we can have an infinite number of iterations.

I think the distinction is related to the one between data and co-data.

>Well, why would it be taken as a given that programming should mimic the hardware?

Because that’s the environment that programs are run on, doing anything else is fighting against the environment. I would argue that humans have done this to great effect in some areas, but not in programming.

>Pure functions are easier to reason about (there may be exceptions of course), that's why they're interesting.

Prove it.

> doing anything else is fighting against the environment

Video game programming, where performance really matters, is a great way to see the cost of forcing the hardware to deal with human abstractions (mainly OOP). Rules like "never have a Boolean in a struct" or "an array with linear access can be faster than a tree with log access" wake you up to the reality of the hardware. :p

In academia, and the especially academic, utopian realm of functional programming, you're trained to live in dreamland.

If you can afford it, though, hey, it's a nice place to be.

> In academia, and the especially academic, utopian realm of functional programming, you're trained to live in dreamland.

OO outside of contexts where every little bit of performance matters suffers in exactly the exact same way.

> If you can afford it, though, hey, it's a nice place to be.

No arguments there! A huge majority of applications can afford to be written this way, even ones where performance is a concern (WhatApp, for example).

> A huge majority of applications can afford to be written this way, even ones where performance is a concern

This is sometimes true for any one given app but it's not a good overall outcome.

It is why we have today multi-GHz CPUs with lots of cores and dozens of GB of RAM and yet... most actions feel less responsive today than in 1995 with a 120MHz CPU, 1 core and 1MB.

My comment was in response to the need to squeeze out every last bit of performance you possibly can. You're talking about ignoring performance altogether which is not what I'm talking about.

Then again, abstractions can be helpful too, including in game programming. Epic's heavily invested, for example. Or in databases, relational algebra often beats out an array with linear access. I agree that OOP-in-the-small lacks mechanical sympathy though. That's one reason for entity-component-model, though another, I'd argue, is that it provides abstractions that are easier to reason about.

On Epic's case it helps that Tim Sweany started his game company doing games in VB, and always cared for a good developer experience, that is why Unreal Engine always favoured good abstractions, has a C++ GC, Blueprints and now Verse.

He was never a kind of "lets keep doing C in games" style of developer.

Thankfully, without the likes of Unreal, Unity and similar efforts, we would still be doing like it always was done here, kind of mentality.

Andrew Kelley has a pretty good talk on gaining performance in the zig compiler.

In many cases performing math again is faster than memoization.

General gist is to try to cram as much in to the cache lines as possible, sometimes even at the “cost” of calculating values again.

Jax and Daxter did pretty well for a game written in Common Lisp.

And apparently Epic belives enough on this to create Verse, and to quote Tim Sweany point of view on "The Next Mainstream Programming Languages",

http://lambda-the-ultimate.org/node/1277

>Prove it.

Proofs are good evidence that pure functions are easier to reason about. Many proof assistants (Coq, Lean, F*) use the Calculus of Inductive Constructions, a language that only has pure, total functions, as their theoretical foundation. The fact that state of the art tools to reason about programs use pure functions is a a pretty good hint that pure functions are a good tool to reason about behavior. At least, they're the best way we have so far.

This is because of referential transparency. If I see `f n` in a language with pure functions, I can simply lookup the definition of `f` and copy/paste it in the call site with all occurrences of `f`'s parameter replaced with `n`. I can simplify the function as far as possible. Not so in an imperative language. There could be global variables whose state matters. There could be aliasing that changes the behavior of `f`. To actually understand what the imperative version of `f` does, I have to trace the execution of `f`. In the worst case, __every time__ I use `f` I must repeat this work.

And if I go to a flat earth conference, I will find that they produce lots of “proof” for flat earth.

I don’t really accept “this group of people who’s heads are super far up the ‘pure functions’ ass choose purity for their solutions” as “evidence” that purity is better.

I’m not saying that purity is bad by any stretch. I just consider it a tool that is occasionally useful. For methods modifying internal state, I think you’ll have a hard time with the assertion that “purity is easier to reason about”.

>For methods modifying internal state, I think you’ll have a hard time with the assertion that “purity is easier to reason about”.

Modeling the method that modifies internal state as a function from old state to new state is the simplest way to accomplish this goal. I.e., preconditions and postconditions.

There are many situations where the extra constraints on pure functions are very useful. Pure functions can't segfault. They can't overwrite memory used by other parts of your program due to stray pointer references. They can't phone home to Google. Verification and optimization is often much simpler when you know that some functions are pure. Reactive programming frameworks that execute callbacks in response to events can cause really weird bugs if the callback mutates state somewhere. I could go on and on. Nobody is arguing for pure functions all the way down. A program's top-level functions will usually be side-effecting, and then you can call out to pure code any time. In practice, a surprising amount of application logic can end up being pure functions.

>Reactive programming frameworks that execute callbacks in response to events can cause really weird bugs if the callback mutates state somewhere

What's the point of a callback that doesn't mutate state somewhere?

It allows you to separate non-stateful business logic from the stateful update logic. Reactive frameworks usually handle the state mutation for you, eliminating the potential for UI glitches where something that depends on the updated state doesn't get recomputed/redrawn.

A lot of “dependency injection” type frameworks run this way.

The framework or runtime calls your function, and the return value tells it what to do next.

Prominent examples include React and Excel.

Because a stateless program can execute in only one way for any given inputs.

A stateful program can execute in 2^n different ways for each bit of state for any given inputs.

> 2^n

If it only computes from an expression to an expression. I think the bound might be higher if you use imperative statements (/effects).

You can fill the whole 2^n output space by calling random(). But in addition to that, the program might also delete an arbitrary file, or deadlock, etc.

As you say, you cannot make a 100% side-effect free program, unless it doesn't do anything at all.

But I do think it's valuable to aim for as side-effect-free as possible, and concentrate the statefulness into certain part(s), rather than spread out all over the place, which is the typical way typical.

Practicing software architecture should generally lead you to minimize side effects and efficiently manage sections of state small enough to fit into your working memory IMO.

FP can be used to get you there, but it strongly optimizes for readability of experts in most cases which harms readability in general, as there are always fewer experts.

At least that's been my experience with FP languages in the professional space. People often underestimate the benefits of good tooling, a large community, and deep candidate pool.

> it strongly optimizes for readability of experts in most cases which harms readability in general

Strongly disagree. In the way you speak of "readability", you're confusing simplicity and familiarity, which are really two different things.

If FP if not "familiar" to you, then it will require some effort on your part, sure. But you can teach FP to an absolute beginner, and they will likely find it just as simple, if not simpler, than an imperative mode of reasoning. It's basically just a social and cultural issue at this point.

Very much so to all of this. When I started programming I was just messing around and doing so as more of a curiosity than anything. What I came up with on my own was much closer to FP. When I started to really learn and was presented with OO, it took me what felt like a really embarrassingly long time to under how classes worked and why I'd want them. Once I grokked it I had a grand ol' time, but then I learned a functional language and it felt so good to learn an actual well-designed version of how I initially imagined programming should be :)

No programming languages have side effects. Side effects are introduced by the runtime.

All programming languages have side effects. The question is what logical constraints limit them.

Absolutely.

It's often helpful to distinguish between effects and side-effects. The idea is that an effect is deliberate and explicit, such as, say, sending an email or moving a robot's arm. Whereas a side-effect is one that happens but wasn't your explicit objective - heating the CPU, say, or silently caching a value in thread-local storage. Haskell programs often use the type system to make these kinds of distinction.

I’d rather a language is designed to accommodate the human mind, and work back from there through the compiler to figure out how to map that to the capabilities of the hardware, than the reverse.

Speaking for myself, when I’m mentally modeling how I logically work through a problem, which concepts I’ve allocated, used, and freed are not a part of my thought process.

That’s highly dependent on the kind of software you write.

Some software necessitates the programmer thinking about memory usage and optimization (games, simulations, machine learning, etc)

Thinking about memory usage and optimization is the role of the compiler. The fact that some software necessitates the programmer thinking about it is just a consequence of current technology.

I don’t think that’s true.

There are some cases where novel memory layouts are necessary. Especially in graphics programming where you need to, at times, cleverly lay out memory to use the most of every available buffer to create arbitrary visual effects.

Compilers can’t automatically create novel layouts.

That's 0.00001% of the effort of programming.

You also need custom hardware sometimes, like TPUs. That doesn't make software unimportant.

We've been waiting for a "sufficiently advanced compiler" for a very long time. If you're going to write programs for real computers, using real compilers, sometimes you have to care about such things. (If you're going to write programs for hypothetical computers, using hypothetical compilers, such constraints don't apply to you. Have fun running them, though...)

That is absolutely and totally true, but 99.9999% of engineers are probably working on things like web apps or other high-level code.

The argument for FP was never that it was perfectly well-suited to every application-- merely that it was better-suited for your "typical" engineering tasks of writing business logic. FP, proof languages, and logic programming, are also all uniquely well-suited in situations that require correctness and formal verification (safety, aerospace, testing, etc).

To make a very broad, sweeping statement: if your project has a `node_modules` or a `venv`, then FP is the medicine you didn't know you needed. If you're writing low-level metal code / assembly, then you should already know you're not the target audience.

The software world is larger and more diverse than you think.

Maybe on HN 99% of people work on web.

In reality probably like 70%

Even if that's true, does it change anything about the point I made?

No, but I’m also not sure what your point has to do with what I was saying

> I’d rather a language is designed to accommodate the human mind

Agreed, but is FP that?

When I write instructions to someone who does not know how to do something (like for my young kid or an aging parent on using some tech they're no familiar with) it will be strictly procedural. Step 1 do this, then step 2 do that, etc.

> Why is this taken as a given to be a good thing?

It is not taken as a given at all. It is an acknowledgment that it makes perfect sense to build on top of centuries of work and theory on well-behaved tools, rather than reinventing the wheel with ill-behaved tools.

It's honestly wild to see this even being argued about in 2024. Ten years ago, I remember the discussions around FP being universally "yes of course it's better, but what's the best way to make it practical in the real world where you need side effects".

There are folks that think they can still reason about code being executed on 128 cores (AMD EPYC™ 9004).

I mean it's pretty trivial if you have referential transparency, which is what FP gives you.

Indeed, that is the point I am making.

> Why is this taken as a given to be a good thing?

Total programming is not useful for everything. Then again, neither is assembly language, or C++, or Rust, or Python. Each has a particular use case in which they are an appropriate tool, and many use cases in which they are not. The job of an engineer is to figure when each tool is appropriate.

Very good engineers keep tabs on lots of tools so that they can choose the best tool when the time calls.

> I think FP paradigms can be useful in specific problem domains, I'm skeptical of the general utility (vs resource spend) of strong FP languages.

The vast majority of FP languages offer no totality checking. Totality checking is mainly used in theorem provers, which are a small subset of FP. I'm not sure what you're going at here, but you're confusing two separate things.

> Our hardware has state. Any IO is a side effect, so what's the non trivial use case for "pure functions" all the way down?

I think James Mickens in The Night Watch[1] puts it best:

> Pointers are real. They’re what the hardware understands. Somebody has to deal with them. You can’t just place a LISP book on top of an x86 chip and hope that the hardware learns about lambda calculus by osmosis.

[1]: https://www.usenix.org/system/files/1311_05-08_mickens.pdf

You could say the same thing about variables, expressions, statements, and structured programming. It's a lot higher level than assembly language or machine code programming.

> Registers, addresses, and machine instructions are real. They're what the hardware understands. You can't just place an ALGOL book on top of an IBM 709 and hope that the hardware learns about expressions, variables and records by osmosis.

That just means a compiler is required.

What percent of your last program was written in register move commands?

> Why is this taken as a given to be a good thing?

Aspiring to rigorous reason and maximum reasonability is necessary for virtue. Maths is the way we reason rigorously about space and time.

It allows the scalability of algorithms like Star Lisp on the Connection Machine, the abstraction allows algorithms to be easily moved from single thread , to multiple threads, multiple cores, GPGPU.

It is no accident that CUDA and SYCL libraries are written in a functional way, or the AI middleware for compute.

> Why is this taken as a given to be a good thing?

So that we can prove things about software more easily. If we only write stateful imperative programs, we're stuck with tons of Hoare triples and separation logic rather than being able to use equational reasoning or type-driven deductions. For example, this person wrote a parallel wc in Haskell, and they used semigroups to parallelize the word counting.

https://chrispenner.ca/posts/wc

Very big difference between pure and total functions.

Pure functions are memoryless and deterministic.

Total functions are defined for all elements in its domain.

Square (x²) is a total function. Reciprocal (1/x) is not, since 0 is a real number, but has no reciprocal.

“Total” and “pure” are orthogonal concepts.

A pure functions that raises an error with the input 0/0 is not total, and you can have total functions that aren't pure.

> Total functions are defined for all elements in its domain.

Do you include "same-output-for-the-same-input" as part of defined?

In context of This paper, where they are talking about Total forms of pure functions, yes

But in general no.

I could say have a total function with an internal counter that adds 1 each time it was run.

That would still be a total function, but not pure.

Yeah I don't think this is a good thing, I also wonder; which mathematics? Mathematics is a big field with wildly different and incompatible notations.

I think there's a lot to discover and apply to programming languages, but the successful result of that will be proving largely procedural programming languages as having certain properties such as memory safety.

Correctness itself is overrated (even in a safety critical field - you always assume the software is faulty and try to make a design that mitigates potential faults). Software is for utility, and even buggy software can have great utility.

> Our hardware has state.

Indeed it does. But why is this opposed to a connection to mathematics?