Groupe "au delà de l'algo-prog"

• on parle peu d'algorithmique distribué (et pourtant cela nous entoure)

• notion d'abstraction:

  • point modélisation, besoin de le décrire, besoin de langage (spécification, description ⇒ langages formels)

  • barrière d'abstraction: interface vs. implémentation, question de la réutilisation

• quand apprendre quoi ?

  • un jour, il faudra construire un curriculum complet de l'informatique, de 5 à 20 ans

    • dans le supérieur:

      • Computer Science Curricula 2013 Curriculum Guidelines for Undergraduate Degree Programs in Computer Science (https://www.acm.org/binaries/content/assets/education/cs2013_web_final.pdf )

      • Programme Pédagogique National DUT Informatique: https://cache.media.enseignementsup-recherche.gouv.fr/file/25/09/7/PPN_INFORMATIQUE_256097.pdf

    • dans le secondaire:

      • au lycée: en seconde et première Informatique et Création du Numérique (http://cache.media.education.gouv.fr/file/CSP/91/2/prog_Informatique_et_creation_numerique_19_mai_425912.pdf) et en terminale Informatique et Science du Numérique (http://eduscol.education.fr/cid59678/presentation.html)

      • enseignant de maths au collège: http://cache.media.education.gouv.fr/file/special_6/52/5/Programme_math_33525.pdf

    • pour les primaires: l'initiative 1, 2, 3 codez de la Fondation la Main à la pâte (http://www.cafepedagogique.net/LEXPRESSO/Pages/2016/06/03062016Article636005337950833622.aspx)

• deux dimensions orthogonales : l'ancienneté des apprenants, et la maturité conceptuelle (à la piaget)

Discussion à part sur une chimère “logique”

But

• comprendre des spécifications pour faire la différence entre “pour tout x, il existe y, ….”, “il existe y, pour tout x, …”

• savoir faire des preuves

• comprendre la notion de “langage formel”

• comprendre la notion de “boite noire” (théorème à utiliser)

Qui ?

• école primaire : modus ponens “s'il pleut, je prends un parapluie. Comme il pleut, alors je prends un parapluie”.

• collège : initiation aux démonstrations avec géométrie

Projet : outil pour construire des preuves niveau collège et lycée

• pouvoir formaliser la conjecture à démontrer

• dessiner des situations géométriques (comme cabrigraph et geogebra )

• pouvoir manipuler / construire des preuves

• il faut des retours du logiciel compréhensible pour l'élève

• s'adapter au programe du collège et lycée, où il n'y a plus trop de démonstrations à produire

  • voir les programmes de maths

• pouvoir évaluer des énoncés dans des situations concrètes

  • à la Tarski's world

  • pratique pour faire la différence entre “pour tout x, il existe y, ….”, “il existe y, pour tout x, …”

  • pt construire des preuves en vrai avec des briques des légos

  • des smartphones sur lesquels sont écrits des énoncés mathématiques que l'on peut placer sur des règles concrètes et ça produit de nouvelles formules

Comment ?

• utiliser Coq ou pas (Coq lourd)

Difficultés

• Problème de l'implication

• Ne pas venir avec notre “vocabulaire”

• Venir avec quelque chose de proche d'eux

• Difficulté pour les élèves de voir dans le plan / l'espace

• inviter les profs à un workshop ? les profs n'ont pas le temps :(

• Evaluation pas faite par les profs mais on reccueille les données

Etat de l'art

• outil existant : Coq et geogebra (voir http://galapagos.gforge.inria.fr/) =⇒ mais difficile à utiliser

• outil mort mais intéressant : https://www-sop.inria.fr/lemme/Frederique.Guilhot/

• Tarski's world

  • Travaux de Julien NARBOUX comme A graphical user interface for formal proof in geometry

  • Geothms, Geometry framework

Specification de l'outil

• tourne dans navigateur

• couplé a Geogebra

• dessiner une figure, formuler une hypothèse, diriger le prouveur avec des indices

• en fait cela existe: Automated Theorem Proving in GeoGebra: Current Achievements et la page correspondante sur Geogebra

Justifications

• compétences utilisées

  • description (ou fourniture) d'une scene geométrique en formules (specifications, modélisation) ou representation géométrique d'une specification

  • formulation (ou fourniture) d'une hypothèse a prouver (but)

  • direction d'un robot prouveur (fourniture d'indices, suivi de la visualisation de l'avancement de la preuve)

Autres idées

• Décrire le niveau de jeu avec une formule logique (logique ATL pour décrire les scénarios possibles)