Is there a proof that runST is indeed pure? : <p>The <a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Monad-ST.html" rel="noreferrer">ST monad</a>, originally devised by <a href="http://dl.acm.org/citation.cfm?doid=178243.178246" rel="noreferrer">Launchbury and Peyton Jones</a>, allows Haskell programmers to write imperative code (with mutable variables, arrays, etc.) while obtaining a pure interface to that code.</p>

<p>More concretely, the polymorphic type of the <a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Monad-ST.html#v:runST" rel="noreferrer">entry point function</a></p>

<pre><code>runST :: (forall s. ST s a) -&gt; a
</code></pre>

<p>ensures that all side-effects of the <code>ST</code> computation is contained, and the resulting value is pure.</p>

<p>Has this ever been rigorously (or even formally) proven?</p>
