Take any Turing-complete programming language and any useful consistent formal system $S$ ("useful" meaning that it has a proof verifier and interprets arithmetic). Then (as described in the linked post), given any program $P$ and input $X$, if $P$ halts on $X$ then $S$ can prove the output. In fact (omitting the coding and interpretation function for convenience) there is a $3$-parameter $Σ_1$-sentence $run$ over PA such that:
For any program $P$ that halts on an input $X$:
$S \vdash run(P,X,P(X))$.
$S \vdash \neg run(P,X,Y)$ for every string $Y \ne X$.
For any program $P$ that does not halt on input $X$:
- $\mathbb{N} \vDash \neg run(P,X,Y)$ for every string $Y$.
For any explicitly primitive recursive program $P$ (using only for-loops):
- $S \vdash \forall x\ \exists y\ ( run(P,x,y) )$.
For any program $P$ on input $X$ that reaches a simple infinite-loop code:
- $S \vdash \neg \exists y\ ( run(P,X,y) )$.
For any programs $P,Q,R$:
$S \vdash \forall x,y\ \Big( run(( t \mapsto \text{if $P(t)$ then $Q(t)$ else $R(t)$} ),x,y)$
$\quad \quad \quad \quad \leftrightarrow \exists z\ ( run(P,x,z) \land z \ne 0 \land run(Q,x,y) ) \lor ( run(P,x,0) \land run(R,x,y) ) \Big)$.
For any program $P$ that halts on input $X$:
- $S \vdash \forall w\ ( run((t \mapsto P(X)),w,P(X)) )$.
Also, for any program $P$, define $total(P)$ to be the sentence $\forall x\ \exists y\ ( run(P,x,y) )$.
Firstly, if $S$ is $Σ_1$-sound, then given any program $P$, if $S \vdash total(P)$ then $P$ is total, because for every (standard) string $x$ we have $S \vdash \exists y\ ( run(P,x,y) )$ and hence $\mathbb{N} \vDash \exists y\ ( run(P,x,y) )$, which implies by (2) that $P$ halts on $x$. Similarly, if $S \vdash \neg total(P)$ then $P$ is really not total, because by (2) we have $\mathbb{N} \vDash \forall y\ ( \neg run(P,x,y) )$.
But (assuming just consistency of $S$) there is a total program $Q$ such that $S \nvdash total(Q)$. Let $φ$ be a $1$-parameter $Δ_0$-sentence over PA such that $\mathbb{N} \vDash \forall x\ ( φ(x) )$ but $S \nvdash \forall x\ ( φ(x) )$, which exists by the incompleteness theorem (as shown in the linked post). Then let $Q$ be a program that uses primitive recursion to evaluate $φ$ on the input string and then halts if it is true but loops forever otherwise. $Q$ is total, but $S \nvdash total(Q)$, because $S \vdash \forall x\ ( φ(x) \lor \neg \exists y\ ( run(Q,x,y) )$ by construction of $Q$ and (1),(3),(4),(5).
And there is also a non-total program $R$ such that $S \nvdash \neg total(R)$. This is because we can construct a program $H$ that, given as inputs a program $R$ and string $X$, simultaneously does the following:
(a) Simulate $R$ on $X$ and output $1$ if $R$ halts on $X$.
(b) Search for a proof of $\neg total((t \mapsto R(X)))$ over $S$ and output $0$ if such a proof is found.
If $S \vdash \neg total(R)$ for every non-total program $R$, then $H$ always halts on every valid input pair. If $R$ does not halt on $X$, then (a) never terminates. If $R$ halts on $X$, then by (6) $S \vdash total(t \mapsto R(X))$ and hence (b) never terminates by consistency of $S$. Thus $H$ always outputs the correct answer, contradicting the undecidability of the halting problem.
The above shows in particular that no useful consistent formal system can prove totality of every total program. One might think that perhaps we could find a slightly less useful consistent formal system that does not interpret Robinson's arithmetic and hence escape the incompleteness theorem. But if you look at the proof of the incompleteness theorem again you see that all $S$ needs to be able to do is to correctly prove output of a program that halts on an input, as stated in (1). So at its core it is not even about arithmetic but whether or not you can verify a finite computation! Also, (3),(4),(5),(6) are other basic properties that we ourselves are capable of identifying about a program, so it would be ridiculous if our formal system is unable to. Note that (2) is not used to show that there is a total program that $S$ cannot prove is total.
Best Answer
Nature of incompleteness
A computational system is said to be Turing complete if the system can be used to simulate an arbitrary Turing machine on an arbitrary input string. Since $\lambda^{\rightarrow}$ is strongly normalizing, every well-typed program is guaranteed to reduce to an irreducible normal form (which is to say, every program halts). As such, we couldn't possibly write a $\lambda^{\rightarrow}$ program to simulate a Turing machine on an input for which the machine never halts; all $\lambda^{\rightarrow}$ programs halt and such a Turing machine on such an input, trivially, does not.
Less formally, simulating arbitrary Turing machines on arbitrary inputs means you need some form of conditional choice (so as to emulate the tape head's ability to move along the tape), and some means of storing and manipulating an arbitrary number of memory locations (so as to emulate the tape). For $\lambda^{\rightarrow}$, typing rules are sufficient to encapsulate the notion of choice, but we can't operate over arbitrary amounts of memory because types can't recurse.
Counterexamples to typability
As far as things that can't be expressed using $\lambda^{\rightarrow}$, a classic example would be fixed point operators. Consider for instance Y combinator, which is defined as $λf.(λx. f(xx))(λx. f(xx))$. Notice that within $(xx)$, we cannot assign a unique type to both occurrences of $x$.
An answer to a similar question on the CSTheory site suggests a more clever example: the function which takes a computable function argument and returns its Gödel number. In this case again, self-reference plays a central role and using a diagonal argument one can prove that a simply-typed term for such a function cannot exist.