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/education/CS2013-final-report.pdf )
      • Programme Pédagogique National DUT Informatique: http://www.iut-orsay.u-psud.fr/_resources/Formations/PPN-Informatique.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)