On construit un cadre, appelé maintenant « réalisabilité classique », pour explorer la correspondance de Curry-Howard (preuves-programmes). Le côté « programmation » de la correspondance est un langage impératif de bas niveau, basé sur une machine lambda-calcul en appel par nom. Le côté « preuve » est la formalisation habituelle de l'Analyse en logique du second ordre. On obtient ainsi des programmes pour toutes les preuves classiques de theorèmes d'Analyse. Pour certains d'entre eux, on résout le problème de la « spécification » : trouver le comportement commun de tous ces programmes, pour un théorème donné. On montre que l'axiome du choix dépendant (qui est essentiel pour l'Analyse) correspond, en programmation, à des instructions très simples : l'horloge et la signature.