Be careful, &#x27;lest your macro language itself turn Turing-complete.<p>&gt; <i>It is not worth sacrificing verifiable correctness to induce this kind of gain when there are better ways of doing it.</i><p>It&#x27;s also important to remember it&#x27;s not always worth sacrificing power to gain verifiable correctness. Not every class of problems needs it.<p>&quot;Freedom for security&quot;, something something. ;).