Constructing a functional on space of bounded operators on separable Hilbert space Let $B(\ell^2)$ be the space of bounded linear operators on the separable Hilbert space $\ell^2(\mathbb N)$. Take any non-zero bounded operator $T\in B(\ell^2)$. By the Hahn-Banach theorem, we can obtain a bounded linear functional of norm $1$ on $B(\ell^2)^*$ that sends $T$ to $\|T\|$. However, is there a way to do this constructively, or at least "more" constructively in some unspecified sense?
If $\|Tx\|$ achieves a maximum at a point $x$ of norm 1, we can define $l(S) = \frac{1}{\|T\|} \langle Sx, Tx \rangle$ and are done. However, most operators won't have this property. We might be tempted to try saying that if instead we only have $\|Tx_n\| \to \|T\|$ for $\|x_n\| = 1$, set $l(S) = \lim_n \frac{1}{\|T\|} \langle Sx_n, Tx_n \rangle$ - but of course this limit might not exist for every operator $S$. Is there some way to do this in a uniform way for all $T$ that actually works? Or do we really need to rely on Hahn-Banach?
 A: There are models in ZF (that is, without choice) where the dual of $\ell^\infty(\mathbb N)$ is $\ell^1(\mathbb N)$.
So let us consider Ryszard's example in this context, where $T$ is the diagonal operator with diagonal $\{(1-\frac1k)\}_k$. Suppose that we have $\varphi\in B(\ell^2(\mathbb N))^*$ with $\|\varphi\|=1$ and $\varphi(T)=\|T\|=1$.
We can identity $\ell^\infty(\mathbb N)$ with the subalgebra $D$ of diagonal operators; restricted to $D$, $\varphi$ can be seen as an element of $\ell^\infty(\mathbb N)^*$. In our model there exists $y\in\ell^1(\mathbb N)$ with $\varphi(x)=\langle y,x\rangle$ for all $x\in\ell^\infty(\mathbb N)$. Then the following happens: with $d$ the diagonal of $T$,
$$
1=\|d\|_\infty=\varphi(d)=\sum_{k=1}^\infty\big(1-\tfrac1k\big)y_k
\leq\sum_{k=1}^\infty\big(1-\tfrac1k\big)|y_k|\leq\sum_{k=1}^\infty|y_k|=\|\varphi\|=1.
$$
The last inequality is then an equality, so
$$
0=\sum_{k=1}^\infty\tfrac1k\,|y_k|.
$$
This is only possible if $\varphi=0$. This shows that in this model no nonzero linear functional on $\mathbb C\,T$ can be extended to a bounded linear functional on all of $B(\ell^2(\mathbb N))$.
In summary, some nontrivial set theory (beyond ZF) is needed, whether it is Hahn-Banach or not; you cannot expect a constructive argument.
