• [^] # Re: prouveur automatique/assistant de preuve

    Posté par (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.

    J'aurais dû préciser que ce programme exécutant tous les programmes ne les exécutera pas jusqu'au bout pour la plupart. L'important est que si on lui offre suffisamment de ressources, il les exécute tous. C'est plus les implications philosophies qui sont intéressantes, et pas l'idée de le réaliser un jour :)

    Pour faire cet énumérateur de programme, on ordonne les programmes par longueur, puis:
    - x = 1
    - t = 1
    - on exécute t secondes de chaque programme de taille <= x
    - on incrémente t et x
    - on répète infiniment

    À l'infini, on a exécuté tous les programmes. Évidemment c'est inatteignable par manque d'énergie pour faire tourner un ordinateur infiniment, mais par contre au bout de "longtemps" on aura probablement simulé toutes les consciences humaines vivantes aujourd'hui. Plus quelques autres.