> Is the forgoing the excluded middle really gaining you the guarantee of computability? It doesn't follow; that uncomputable things cannot be expressed in a c

> Is the forgoing the excluded middle really gaining you the guarantee of computability? It doesn't follow; that uncomputable things cannot be expressed in a constructive system doesn't mean that everything that is computable in principle is also computable, or even definable, in that system (unless by "guaranteeing computability" you meant something else).