I've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages:
1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want)
2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck.
Of course extraction has its own benefits. Coq is a pretty cool tool :)
1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want) 2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck.
Of course extraction has its own benefits. Coq is a pretty cool tool :)