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?