I don't think it really helps software development, if instead of "here's the description of what we need to do" the SW developer gets "here's a few examples of what we need to do" (albeit if the examples can be automatically verified).

If that's NOT your intent, what's the role of specification in the TDD, and how it's interacting with the implementation and the tests?

That's pretty much it. The value is that tests can be automatically executed and verified. A specification document can't.

Writing a spec is still a step in the process - a bootstrapping step. The spec is a "write one to throw away" placeholder until you get far enough that the spec can be replaced with executable tests.

My take on specification is that you encode it to be executable as your program, during development. Ideally, the program should encode the specs in the most straightforward way possible. To "specialize" the spec into tests first and then "generalize" it again from tests into a working program seems like unnecessary hassle, and frankly prone to information loss.

It's interesting, because as I state in another comment, I have a big disagreement with a guy who loves TDD. I guess I am a theorist (I derive my feeling of correctness from simplicity of the code) and he is an empiricist (he derives his feeling of correctness from many small tests), and it somehow defines our approach.

The adherents really want tests to be the specification, as a way to be measurable / testable. Specs may be converted to tests.

But most of it is theory. It all depends, as usual, on the dev(s) and circumstances.