Hmm, I find TLA+ to be very user-friendly. It's one of its major strengths (it was very important to Lamport to observe engineers as they learn and apply it). It is certainly easier than learning Haskell, or even OCaml or Rust. I think it's a bit like Lisp: it's a minimal language with
very few concepts, that may be unfamiliar at first and take a bit to fully wrap your head around, but once you do, you have unlimited power. I think that you can become seriously productive in it after about two weeks. All the
tricky concepts (the TLA part of TLA+) are explained in this very short text[1] (I haven't seen the operator introduced in the Assumption/Guarantee section used in a spec). When you get those, you know TLA+
well, the "+" bit is
very easy; a little like Clojure, only simpler.
It's not only easy to learn, it's extremely powerful, mostly due to refinements (an advanced concept, better left for week 3 :)), which are absolutely necessary for large systems/algorithms.
There are also two breakthroughs in TLA, which you may come to appreciate: the expression of the program and the program's properties in the same minimal language, and the demonstration that simple, high-school math, plus one or two new concepts, is all it takes to specify and verify programs.
And yeah, code extraction from specification is an open research question, but I don't even consider this to be a top-ten desired feature, considering the amount of time spent specing and verifying vs. translating to the implementation language.
[1]: http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1994-001...