[gjem97]

Presumably one of the applications of a compiler with a built-in theorem prover is mission critical code. But my understanding is that most mission critical code environments prohibit recursion. What's the main target usage here?

[mmalone]

I've never worked on something "mission critical," but most common uses of recursion are tractable, so I'm not sure why it would be disallowed.

The simplest form of tractable recursion is where some argument in the recursive call is, by some metric, "smaller" than the outer call, and is heading towards a base case that terminates recursion when the argument reaches "zero." Two examples are: decrementing integers towards zero, and recursing on the tail of a list. You can prove termination and many other properties of such a function by induction. This concept is fairly easy to generalize to any algebraic data type, and to many other domains.

Edit: I realized I didn't really answer your question. The folks who are working on dependently typed languages (like Idris) see them as broadly useful, and they have a good point. Consider Java generics: they let you have types that depend on other types, like a "List of Integers." The compiler can make guarantees based on that type information and a lot of people consider that useful. With dependent types you can have types that depend on _values_, like "List of exactly 5 Integers that are all between 0 and 100." Again, the compiler can make guarantees based on that type information, and it could improve code safety, modularity, etc.

The challenge with dependently typed languages has been coming up with a "surface syntax" that's easy to use. Idris (and Agda) are pretty much state of the art there.

[regularfry]

"most common uses are tractable" does not guarantee that many common uses will have been correctly analysed.

As to why it's disallowed: stack space is limited, and tail call optimisation isn't taken for granted. Here's what the Joint Strike Fighter coding standards (thataway -> http://www.stroustrup.com/JSF-AV-rules.pdf) say:

    AV Rule 119 (MISRA Rule 70)
    Functions shall not call themselves, either directly or indirectly 
    (i.e. recursion shall not be allowed).

    Rationale: Since stack space is not unlimited, stack overflows are possible.

    Exception: Recursion will be permitted under the following circumstances:

    1. development of SEAL 3 or general purpose software, or

    2. it can be proven that adequate resources exist to support the maximum level of
    recursion possible.

So yes, you're allowed it if you do that extra work, but given that you can replace tractable recursion with a loop anyway, the win you'd have to get from expressing the problem recursively has to compensate.

[mmalone]

Interesting. Thanks for the details.

In theory a compiler can do this optimization for you and can use simple syntactic checks to determine whether recursion terminates and whether the optimization applies (at least given a language designed with these things in mind, I'm sure this is much harder or maybe impossible in C++). With something more modern than C++ I'd imagine you could adopt a rule that says "you can use recursion but we compile with --dont-allow-nonterminating-or-unoptimizable-recursion".

[rs86]

Why does it prohibit recursion? Tail call optimization can prevent stack overflow

[regularfry]

Can if it's present. "Mission critical" tends to mean c/c++ where chances are you've got to do that sort of thing yourself.