Axiomatic Programming is commonly defined as structured generic programming. Not unlike Euclidean Geometry, it relies on a simple, constructive, logical system. It lies at the foundation of the STL and many successful generic libraries. This talk focuses on tools support and illustrates how ideas and methods from automated deduction and proof theory influence current and future possible developments of C++ templates.