Well, as you go to the next steps you can use proof search techniques to do exactly that: write your types and your programs write themselves as the "only possible implementation".
This is already possible sometimes in Haskell so long as we restrict ourselves from pathological values like exceptions and non-termination. In fact, the first place this phrase shows up is Russel O'Connor talking about highly polymorphic lens code.
This kind of type limitation of possible implementations is called parametricity and is difficult to encounter even in most typed languages as it requires purity.
In practice types often winnow the possible implementations to be a relatively small set. This effect is improved if you also include notions of law-abiding implementations as Haskellers often do. At the end of the day, it's true that implementations (don't yet) write themselves, but, more realistically, that the constraints of type and theory drive you naturally to the correct solutions even if you never once figure out the "operational" aspect.
I don't think anyone believes that types are sufficient outside, at least outside of a dependently typed language (at which point you'll have more diversity of opinion).
This is already possible sometimes in Haskell so long as we restrict ourselves from pathological values like exceptions and non-termination. In fact, the first place this phrase shows up is Russel O'Connor talking about highly polymorphic lens code.
http://r6.ca/blog/20120708T122219Z.html
This kind of type limitation of possible implementations is called parametricity and is difficult to encounter even in most typed languages as it requires purity.