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
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)