DeVault: Announcing the Hare programming language

<p>I mean something which was done for safe Rust: formal mathematical model which may prove that transformation which are done during optimizations are sound.</p>

<p>Things like <a href="https://www.ralfj.de/blog/2020/12/14/provenance.html">that</a> should be impossible.</p>

<p>Today optimizations in compilers are dark art: not only they produce suboptimal code sometimes (that's probably something which we would never be able to fix), we discover, from time to time, that they are just simply invalid (as in: they turn perfectly valid programs into invalid).</p>

<p>Ideally we should ensure that all optimizations leave valid programs still valid (even if, perhaps, not optimal).</p>