It is a proof that we can get what we need to done in a language that is not Turing complete.  The hope would be that there is some sweet spot we can find wherein we can say things that are dramatically more useful than &quot;it will finish inside 2^(2^100) steps&quot; without impacting usability tremendously more than &quot;it won&#x27;t use more than a kebibyte of memory&quot; - which is already enough to defang the theoretical objection.