[Musser] Currently, in both the ANSI/ISO C++ standard and the SGI STL concept web, the semantics of the STL components is given only informally as a set of requirements stated in English. While there are some devices used that aid in achieving completeness and precision, particularly the use of concept refinement in the SGI concept web, these specifications remain incomplete and somewhat vague, depending heavily on reader's (and library implementor's) prior knowledge and "good intentions." STL presents an opportunity for formalists to try their techniques on a library that is important to a large community of programmers.
Two lectures at the Dagstuhl seminar that addressed this problem were those by Gary Leavens and Alexandre Zamulin.