String library: should it be built on top of the list library? should it be made abstract?

It was advocated that the use of a concrete but ad hoc structure of list in the String library was the worst possible design and that it should either be entirely built on List (to take benefit of the List library), or made abstract so that String could be directly extracted to the primitive type string of the languages targetted by the extraction.

This seems to be a reasonable position, and, actually, both directions could even be adopted, with a List-based implementation hidden behind an abstraction, with only drawback to have to express computational rules as abstract equations, and, mitigating this e.g. by providing a corresponding autorewrite database.

This issue is to collect further opinions on the design of the String library and to eventually provide a new one. [Note that I'm not myself a heavy user of the String library, so, the point is rather to collect inputs from heavy users.]

Start by reading the linked PR discussion and comparing the current String and List library designs. A useful outcome would require a decided design and concrete scope for a replacement or abstraction; the issue names no files or tests.