For your world, I think FP is a bad idea. GC is a bad idea. (Allocations after startup are a bad idea, too, and a language that allocates without being asked is a terrible idea.) Recursion is a bad idea. (Yes, tail-call-optimization can essentially turn it into recursion. Mis-write one TCO in the whole program, though, and your stack just became extremely unpredictable.) And considering Haskell specifically, in your world lazy is a terrible idea.

FP is a tool. It has potential to solve some problems. That potential won't be wasted, but the problems it will solve aren't the problems you have in your world.

On the other hand, FP could be just fine for writing the tools that will help you in your world.

FP is good idea for safety critical systems. It just has to be designed differently.

You want uniqueness typing that allows you to have functions that modify the variables without breaking the functional abstraction in straight forward manner. You could also reason about the memory use and have fixed amount of memory. Ordered typing would be nice feature to have. You also want hooks in the compiler for a additional tools for static analysis and proof assistants.

Recursion itself is not bad idea. It's strictly forbidden in safety critical code today for reasons that can go away. If you allow recursion, compiler must be able to reason and define the limits. Recursion is not good idea in safety critical code when it obfuscates the execution, but that is not always the case.

If I understood what you said correctly, you could have FP that allowed (controlled) mutation of the existing variable rather than allocating a new one. I suppose that could be done. But it seems to me that many people regard immutability as an essential part of FP, because without immutability, composability is no longer guaranteed. So to get what you'd like FP to be, you may have to step outside the existing FP community.

The essential part of what makes FP FP is referential transparency not immutability. Having referential transparency with mutation is what the uniqueness typing provides.

> Recursion is a bad idea

Raw recursion or recursion using recursive schemes?

Any recursion. The problem is that, without tail call optimization, you create one stack frame per recursion. In Nokinside's world, you have to prove that you will never exceed the stack size. To prove that, you have to prove an upper bound on the number of recursion calls, and multiply by the size of a call's stack frame. Proving it for iteration is much easier, partly because (under the MISRA C rules or similar) iterations must have fixed bounds, but mostly because you don't create a stack frame for each iteration.

My turn: What's a recursive scheme?

> Writing MISRA C and using verification tools like Astree, or SPARK + verification tools are not as elegant, but their weakest point is stronger than Haskell's.

That's why we need more Haskell-hosted system programming DSLs - with fancy sound types, proofs, extraction and stuff.