[wyager]

> No, complex programs by definition don’t fit into human working memory.

If you write your code in the right way they don’t have to. That’s the point.

You shouldn’t need to comprehend your entire program at once to work with it.

> Even with best practices, FP, whatever, function composition alone can’t always elevate the complexity to the requirement’s level

Function composition isn’t the pinnacle of abstraction. We have many other abstraction techniques (like rich types, lawful typeclasses, parametric programming, etc.) which allow for any given subcomponent of a program to be conceptualized in its entirety.

[Jweb_Guru]

> If you write your code in the right way they don’t have to. That’s the point.

I recommend you try working through some equality proofs in Coq, first with and then without coqtop / Proof General. I think you may change your mind about this rather rapidly. And many proofs get much more complex than that.

[wyager]

I’ve used (and developed) plenty of proof assistants. Proofs are one very narrow domain where automation is basically a no-brainer. You don’t really lose out from the proof having high semantic arity. With normal code, you do lose out.

[Jweb_Guru]

I dunno. I think the line between "normal code" and proofs is a lot blurrier than many people make it out to be, and I don't think there's a huge advantage to asking people to run a type checker or inference algorithm in their heads even if you have managed to encode all your program's invariants in the type system (which is impossible or impractical in many languages). I say that as someone who doesn't use an IDE except when I'm forced to: I know I lose out on a lot of productivity because of it, and I don't find that removing the IDE forces me to develop better or more concise code.

[kazinator]

What if the program is a hundred million floating-point values, produced by learning?

Can you look at them in small chunks to understand what they are contributing to the result?

It looks like there is such a thing as complexity that is not functionally decomposable.

[wyager]

Do you write your programs like a neural network? I would consider that a major red flag when hiring.