Hacker News Reader

Systems where you need to prove correctness at least informally. It’s much easier to prove correctness of a functional program than imperative one.

View on HN

Depends on your definition of "correctness". In MISRA, JSF, and similar areas, memory usage (including stack!) is part of the correctness. If you overflow the stack because of recursion, it doesn't matter how "correct" the rest of the program was, it's still broken.

And the same for time. Some programs require proving that you meet the timing constraints. Recursion does not make that easier. (Neither does a language that can allocate behind your back, nor one that can run a garbage collector.)

So the rules for such environments usually say: No recursion, and no allocations after initialization. They say this because those rules make it easier to prove correctness.

Unstructured recursion is incredibly tricky to reason about in terms of stack/heap use and termination, IMO quite a bit moreso than imperative structures. To me, it reproduces most of the same problems of gotos.

There are techniques of factoring out recursion (e.g. "recursion schemes") that can help eliminate these problems, but some things are just easier to reason about imperatively.

Reply on news.ycombinator.com