Is there high-level language out there for describing algorithms, that's geared towards specification, rather than implementation?
The idea would be to have a machine-readable archive of standard algorithms, with machine-readable annotations on trade-offs, and variants.
I'm thinking of something like CycL / OpenCyC, but for algorithms and programming patterns.
The glib answer: Yes. It's called English.
The serious answer: No, as you've probably already assumed after months of this question going unanswered. I don't believe there's any real consensus, or even consideration, over what such a language would entail. Programming patterns and algorithms are always changing and evolving, so designing a language that would be able to describe all future patterns would be very difficult, if not impossible.
Pseudocode, possibly. Or flowcharts. For machine readable, it would have to be something like a meta-language. Lisp and Forth come to mind. Languages that are essentially self-defining, with a small set of primitives to build up the higher layers of abstraction.
These are not exact fits, but they are somewhat close: Maude and CASL. They are both machine-readable (with decent tools) specification languages which also allow some forms of code. Some people swear by AsmL, but I'm not a fan.
Soon I think that Agda 2 will fulfill that niche quite well, but it's still in full development. One can also say that Coq already fulfills that role (because of program extraction), but I am not a fan either.