> My main idea is that as a programmer what I do is constantly reducing the set of all programs to a particular program which satisfies the specification. An a

> My main idea is that as a programmer what I do is constantly reducing the set of all programs to a particular program which satisfies the specification. An alternate point of view is to start with the specification, interpreted as a generally nondeterministic program, and then refine it using logically sound optimizations to render it executable. This is roughly the approach of Fiat: http://adam.chlipala.net/papers/FiatSNAPL17/ http://adam.chlipala.net/papers/FiatSNAPL17/ They’ve used it to generate crypto primitives that are in use: http://adam.chlipala.net/papers/FiatCryptoSP19/ http://adam.chlipala.net/papers/FiatCryptoSP19/