  It is well known that most foundations for Bishop's constructive mathematics
are incompatible with a classical predicative development of analysis as put
forward by Weyl in his $\textit{Das Kontinuum}$. Here, we first recall how this
incompatibility arises from the possibility, present in most constructive
foundations, to define sets by quantifying over (the exponentiation of)
functional relations. This possibility is not allowed in modern formulations of
Weyl's logical system. Then, we argue how a possible way out is offered by
foundations, such as the Minimalist Foundation, where exponentiation is limited
to a primitive notion of function defined by $\lambda$-terms as in dependent
type theory. The price to pay is to renounce the so-called rule of unique
choice identifying functional relations with $\lambda$-terms, and to
number-theoretic choice principles, characteristic of foundations aimed to
formalize Bishop's constructive analysis. This restriction calls for a
point-free constructive development of topology as advocated by P. Martin-L\"of
and G. Sambin with the introduction of Formal Topology. Hence, we conclude that
the Minimalist Foundation promises to be a natural crossroads between Bishop's
constructivism and Weyl's classical predicativity provided that a point-free
reformulation of classical analysis is viable.
