Constructive Mathematics and Termination In the 1988 book The Universal Turing Machine A Half-Century Survey
there is the paper "The Confluence of Ideas in 1936" by Robin Gandy. In section 4.2, Gandy writes:

"If one accepts, on whatever grounds, that a process terminates after a finite number of steps, then one should also accept, on the same grounds, that the number of steps can, in principle, be computed - one only needs a clock![8]"

Footnote [8] states:

"A constructive mathematician may have good grounds for believing that the process doesn't fail to terminate, without believing that it does terminate. Markov used his principle to jump over this gap."

My question is, can there exist a constructive logic and a Turing machine such that 
1) the logic proves that the Turing machine doesn't fail to always terminate and
2) the logic does not prove that the Turing machine does always terminate?
 A: Ingo Blechschmidt already explained in the comments why we should expect a negative answer to the question (for most readings of "constructive logic"). Namely, if classical arithmetic proves $\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$, where $\phi(n,k)$ is quantifier-free, then so does intuitionistic arithmetic. So then, if intuitionstic arithmetic proves $\lnot\lnot \forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$, then so does classical arithmetic, but classically we may remove the $\lnot\lnot$, and then go back to intuitionistic logic to get $\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$. The statement "Turing machine $M$ halts on every input" is of this form, namely
$$\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . T(m, n, k),$$
where $m$ is a code of $M$ and $T$ is Kleene's predicate $T$.
What I would really like to explain is that in a sense this is the wrong question to ask. Let $H(m)$ be the statement that the Turing machine encoded by $m$ always halts, i.e., $$H(m) \iff \forall n \in \mathbb{N} . \exists k \in \mathbb{N} . T(m, n, k).$$ In terms of $H$, the question is: "Is there a number $m$ such that intuitionistic logic proves $\lnot\lnot H(m)$ but does not prove $H(m)$?" This seems to indicate to me that the author of the question is trying to imagine how $$\forall m \in \mathbb{N} . (\lnot\lnot H(m) \Rightarrow H(m))$$ might fail, and he expects to be able to find an instance of $m$ in which the implication fails. But in intuitionistic logic this is not the right way to think of quantification and implication!
The classical reading of $\forall x \in A . \psi(x)$ is "$\psi(a)$ holds for every element $a \in A$", whereas the intuitionistic reading of the same statement is "there is a procedure which takes as input any $a \in A$ and outputs evidence of $\phi(a)$. Here the word "procedure" is not fixed: it cold mean a computable map, or a continuous map, or computable with respect to an oracle, etc. But the point is this: in intuitionistic logic $\forall x \in A . \psi(x)$ may fail because there is no procedure, and not because there is a specific $b \in A$ for which $\lnot \psi(b)$ holds.
Applying the last paragraph to Markov's principle, we see that the "correct" question to ask was:

Is there a procedure which takes as input (the code of) a Turing machine $M$ that never runs forever, and a number $n \in \mathbb{N}$, and halts and outputs the running time of $M(n)$?

