Das Argument mit dem Halteproblem kann ich nicht nachvollziehen. Abgesehen von dem begrenzten Speicher sollte es problemlos möglich sein, eine Turingmaschine zu realisieren. Schließlich bieten die Contracts keine Aussage über die Laufzeit.
Doch, das ist theoretisch schon ein Problem. Angenommen, dein Contract wäre, dass ein kryptographischer Hash des Parameters nicht 0 sein darf. Also z.B. SHA1(Parameter) <> 0. Viel Spaß dabei, zur Compilezeit auszuwerten, welche Werte erlaubt sind.