How to auto-derivate sequential iterative programs from a mathematical specification?
Short answer: no.

Long answer: No, because the synthesis problem is in general undecidable once you allow for a modest amount of expressive power in the assertions (pre- and post-conditions).

The specification for your synthesizer $S$ would look something like this. Its type would be $S:\mathit{Assn}^2\rightarrow\mathit{Prog}$, that is, given two assertions (a pre- and a post condition) it would return a program. Its functionality would be given by $\{\phi\}S(\phi,\psi)\{\psi\}$, for all $\phi,\psi\in\mathit{Assn}$. I understand your question as "is $S$ computable?"

Before we need to get technical, note that we've been a bit sloppy. $S$ can hardly be a total function for we could feed it an infeasible spec such at $[\mathit{true},\mathit{false}]$. Consequently, the best we could hope for is a partial function that works for all implementable specifications.

To answer the refined question we need to answer another first.

What expressive power would we need in the assertion language?

Firstly, assuming that we're living in a simple world where we only deal with integers, we require the usual operations from integer arithmetic.

Secondly, we need a mechanism to refer in the post-condition to the value of a program variable in the pre-condition. Without such a mechanism, we cannot even specify an increment-by-one function. Various such mechanisms exist. Let us here use one borrowed from the Z specification language: in the post-condition primed occurrences $x'$ of a variable $x$ refer to its value after the program has terminated whereas unprimed occurrences denote its value in the pre-condition. With this convention the increment-$x$-by-one function is specified by $[true,x'=x+1]$.

Thirdly, we'd also want quantifiers so we can at least specify simple examples such as


a primality checker


$[x &gt; 0, x=x'\land(p\Leftrightarrow x&gt;1\land\forall k(k&gt;1\land \exists j(kj=x)\Rightarrow k=x))]$, and


a sorter that takes arrays of arbitrary size as inputs


$[\mathit{true},\mathit{length}(a)=\mathit{length}(a')\land\mathit{elements}(a)=\mathit{elements}(a')\land\forall i(1\leq i &lt;\mathit{length}(a')\Rightarrow a'[i]\leq a'[i+1])]$.

With those ingredients, we have quite some power at our disposal, too much as it turns out. Even the domain of $S$ is undecidable because we would need to say whether a spec $[\mathit{true},\phi]$ is implementable or not, for arbitrary formulas $\phi$ of Peano arithmetic, before worrying about how to synthesize implementations. But that is already undecidable.