I can write this answer as someone who proves things a lot, so to me correctness isn’t just what works, but what works and is easy to prove.

In a lot of senses, functional programming is more restrictive then imperative programming. After all, nothing stops you from never mutating a variable in C! Indeed most of the features in FP languages are straight forward to talk about in terms of only a few core features. It all pretty much boils down to lambdas, function application, and pattern matching!

However, since we’ve paid the piper in advance, we have a lot less to deal with and we have a lot less options for how things can go wrong. If your a 1984 fan, freedom is indeed slavery! By using 101 different neat tricks for a program, we have to reason about things as though any of these 101 things can happen! That’s really hard to do as it turns out 🙂

If you start with safety scissors instead of a sword, running is moderately less dangerous.

Now we look at your question: how does all of this fit into the “it compiles and works!” phenomena. I think a large part of this is the same reason as why it’s easy to prove code! After all, when you write software you’re constructing some informal proof that it’s correct. Because of this what’s covered by your natural handwavy proofs and the compilers own notion of correctness (typechecking) is quite a lot.

As you add features and complicated interactions between them, what’s not checked by the type system increases. However, your ability to construct informal proofs doesn’t appear to improve! This means that there’s more that can slip through your initial inspection and must be caught later.

the underlying abstract reason for the correlation between compilation success and program correctness in functional programming?

Mutable State.

Compilers check things statically. They make sure your program is well formed, and the type system provides a mechanism for trying to ensure that the right sort of values are allowed in the right sort of places. The type system also tries to ensure that the right sort of semantics are allowed in the right sort of places.

As soon as your program introduces state, that latter constraint becomes less useful. Not only do you need to worry about the right values in the right spots, but you also need to account for that value changing at arbitrary points of your program. You need to account for the semantics of your code changing alongside that state.

If you’re doing functional programming well, there is no (or very little) mutable state.

There is some debate though about the causation here – if programs without state work after compilation more frequently because the compiler can catch more bugs or if programs without state work after compilation more frequently because that style of programming produces less bugs.

It’s likely a mix of both in my experience.

To put it simply, the restrictions mean there are fewer correct ways to put things together, and first-class functions make it easier to factor out things like loop structures. Take the loop from this answer, for example:

for (Iterator<String> iterator = list.iterator(); iterator.hasNext();) {
    String string = iterator.next();
    if (string.isEmpty()) {
        iterator.remove();
    }
}

This happens to be the one safe imperative way in Java to remove an element from a collection while you’re iterating through it. There are lots of ways that look very close, but are wrong. People unaware of this method sometimes go through convoluted ways to avoid the problem, like iterating through a copy instead.

It’s not terribly difficult to make this generic, so it will work on more than just collections of Strings, but without first-class functions, you can’t replace the predicate (the condition inside the if), so this code tends to get copied and pasted and modified slightly.

Combine first-class functions that give you the ability to pass the predicate in as a parameter, with the restriction of immutability that makes it very annoying if you don’t, and you come up with simple building blocks like filter, as in this Scala code that does the same thing:

list filter (!_.isEmpty)

Now think about what the type system checks for you, at compile time in the case of Scala, but these checks are also done by dynamic type systems the first time you run it:

• list must be some sort of type that supports the filter method, namely a collection.
• The elements of list must have an isEmpty method that returns a boolean.
• The output will be a (potentially) smaller collection with the same type of elements.

Once those things have been checked, what other ways are left for the programmer to screw up? I accidentally forgot the !, which caused an extremely obvious test case failure. That’s pretty much the only mistake available to make, and I only made it because I was directly translating from code that tested for the inverse condition.

This pattern is repeated over and over again. First-class functions let you refactor things out into small reusable utilities with precise semantics, restrictions like immutability give you the impetus to do so, and type checking the parameters of those utilities leaves little room to screw them up.

Of course, this is all dependent on the programmer knowing that the simplifying function like filter already exists, and being able to find it, or recognizing the benefit of creating one yourself. Try to implement this yourself everywhere using only tail recursion, and you’re right back in the same complexity boat as the imperative version, only worse. Just because you can write it very simply, doesn’t mean the simple version is obvious.

I don’t think there’s a significant correlation between functional programming compilation and runtime correctness. There may be some correlation between statically typed compilation and runtime correctness, since at least you may have the right types, if you’re not casting.

The programming language aspect that may somehow correlate successful compilation with runtime type correctness, as you describe, is static typing, and even then, only if you’re not weakening the type checker with casts that can only be asserted at runtime (in environments with strongly typed values or places, e.g. Java or .Net) or not at all (in environments where the type information is lost or with weak typing, e.g. C and C++).

However, functional programming per se may help in other ways, such as avoiding shared data and mutable state.

Both aspects together may have a significant correlation in correctness, but you must be aware that having no compilation and runtime errors tells nothing, strictly speaking, about correctness in a broader sense, as in the program does what it is supposed to do and fails fast over invalid input or uncontrollable runtime failure. For that, you need business rules, requirements, use cases, assertions, unit tests, integration tests, etc. In the end, at least in my opinion, they provide much more confidence than either functional programming, static typing or both.

Explanation for managers:

A functional program is like one large machine where everything is connected, tubes, cables. [A car]

A procedural program is like a building with rooms containing a small machine, storing partial products in bins, getting partial products from elsewhere. [A factory]

So when the functional machine already fits together: it is bound to produce something.
If a procedural complex runs, you might have overseen specific effects, introduced chaos, not guaranteed the functioning. Even if you have a checklist of everything being correctly integrated, there are so many states, situations possible (partial products lying around, overflowing buckets, missing), that guarantees are hard to give.

But seriously, procedural code does not specify the semantics of the desired result as much as functional code. Procedural programmers may more easily get away by circumstantial code and data, and introduce several ways to do one thing (some of them imperfect). Typically extraneous data is created. Functional programmers might take longer when the problem gets more complex?

A strong typed functional language can still do better data and flow analysis.
With a procedural language, the goal of a program often has to be defined outside of the program, as a formal correctness analysis.