Naturally you first implement your algorithm together with a correctness proof inside the turing-complete type system. After that writing the real implementation can be left as an exercise for the compiler :)

I'm sure that in 1986, before standardizing ANSI C, someone victoriously typed the same thing in front of his tty in a discussion about using types in declarations and not just doing it à la K&R with just the function name being called cowboy-style.

Just because a system does not catches all bugs does not make it useless - for me, even if C++'s type system had caught only one bug it'd be worth it (and in most of my code, which is mainly about fairly specific domain objects, the compiler saves me from myself pretty much daily).

In any case, I'd likely have this somewhere

    constexpr double negate(double x) {
        return -x;
    }
  
    // example implementation for the sake of the comment, there are much more exhaustive libs out there
    constexpr bool sample(auto func) {
        bool ok = true;
        double x = -1000.;
        while(x < 1000.)
        {
          ok &= func(x); 
          x += 1.;
        }
        return ok;
    }

    static_assert(sample([] (double x) { return negate(x) == -x; }));

this way I'd get a compile error if my cat walks on my keyboard and inadvertently removes the - (also a relatively common occurence)

By using contracts, unfortunately they were postponed to C++23.