This is a naïve and, therefore, possibly malformed question, so apologies in advance!

My view is that a Turing Machine can be seen as the computational basis for procedural/imperative programming languages. Similarly, the lambda calculus is the foundation for functional programming languages.

I have recently learnt that the Church-Turing Thesis also shows mutual equivalence with a third model of computation: general recursive functions. Are there any programming languages that use this as their model of computation? If not, is there a technical reason why; i.e., besides "No one's tried yet"?

Direct answer to the question: yes, there are esoteric and highly impractical PLs based on $\mu$-recursive functions (think Whitespace), but no practical programming language is based on $\mu$-recursive functions due to valid reasons.

General recursive (i.e., $\mu$-recursive) functions are significantly less expressive than lambda calculi. Thus, they make a poor foundation for programming languages. You are also not correct that the TM is the basis of imperative PLs: in reality, good imperative programming languages are much closer to $\lambda$-calculus than they are to Turing machines.

In terms of computability, $\mu$-recursive functions, Turing machine, and the untyped $\lambda$-calculus are all equivalent. However, the untyped LC has good properties that none of the other two have. It is very simple (only 3 syntactic forms and 2 computational rules), is highly compositional, and can express programming constructs relatively easily. Moreover, equipped with a simple type system (e.g., System $F\omega$ extended with $\mathsf{fix}$), the $\lambda$-calculus can be extremely expressive in that it can express many complex programming constructs easily, correctly and compositionally. You can also extend the $\lambda$-calculus easily to include constructs that are not lambdas. None of the other computational models mentioned above give you those nice properties.

The Turing machine is neither compositional nor universal (you need to have a TM for each problem). There are no concepts of "functions", "variables" or "composition". It is also not exactly true that TMs are the basis of imperative PLs - FWIW, imperative PLs are much, much closer to lambda calculi with control operators than to Turing machines. See Peter J. Landin's "A Correspondence Between ALGOL 60 and Church's Lambda-Notation" for a detailed explanation. If you have programmed in Brainf**k (which actually implements a rather simple Turing machine), you will know that Turing machines are not a good idea for programming.

$\mu$-recursive functions are similar to TMs in this respect. They are compositional, but not nearly as compositional as the LC. You also just can't encode useful programming constructs in $\mu$-recursive functions. Moreover, the $\mu$-recursive functions only compute over $\mathbb{N}$, and to compute over anything else you'd need to encode your data into natural numbers using some sort of Gödel numbering, which is painful.

So, it is not a coincidence that most programming languages are somehow based off the $\lambda$-calculus! The $\lambda$-calculus has good properties: expressiveness, compositionality and extensibility, that other systems lack. However, Turing machines are good for studying computational complexity, and $\mu$-recursive functions are good for studying the logical notion of computability. They both have outstanding properties that the $\lambda$-calculus lacks, but in the field of programming $\lambda$-calculus clearly wins.

In fact, there are many, many more Turing complete systems out there, but they lack any outstanding property whatsoever. Conway's Game of Life, LaTeX macros, and even (some claim) DNA are all Turing complete, but no one programs (i.e. do serious programming) with Conway or studies computational complexity using LaTeX macros. They simply lack good properties. Turing complete per se is nearly meaningless when it comes to programming.

Also, many non-Turing complete computational systems are very useful when it comes to programming. Regular expressions and yacc are not Turing complete, but they are extremely powerful in solving a certain class of problems. Coq is also not Turing complete, but it is incredibly powerful (it's actually considered much more expressive than its Turing complete cousin, OCaml). When it comes to programming, Turing completeness is not the key, as many (close to) useless systems are uninterestingly Turing complete. You're not going to claim that Brainf**k or Whitespace are more powerful programming languages than Coq, are you? An expressive foundation is the key to powerful programming languages, and that's why modern programming languages are almost always based on the $\lambda$-calculus.
