il s'adresse principalement aux étudiants de première et deuxième année de licence intéressés par l'ingénierie ou les sciences, ainsi qu'aux lycéens et aux professionnels intéressés par la programmation.Design by Provable Contracts vous enseigne comment passer de "les tests passent" à "les maths disent que ça ne peut pas casser" A travers cinq modules, vous gravirez une échelle de prouvabilité à cinq échelons - de lint et types, en passant par property-based et bounded-model checking, jusqu'aux dependent-typed proofs dans Lean 4 - appliquée à un seul exemple courant : la fonction softmax utilisée dans l'apprentissage automatique moderne. A la fin, vous serez en mesure de : (1) lire un article revu par des pairs et traduire ses préconditions, postconditions et invariants en un contrat YAML ; (2) choisir le bon échelon de vérification pour un compromis coût-confiance donné, en utilisant lint, types, proptest et Kani en Rust ; et (3) construire un pipeline complet de l'article au YAML au théorème Lean, produisant une garantie vérifiée par la machine qui tient pour chaque entrée de n'importe quelle longueur. Le cours est pratique et l'outil prime : Rust pour les échelons inférieurs, Lean 4 pour l'échelon supérieur, et YAML comme tissu conjonctif entre les mathématiques et le code. Vous repartirez avec un modèle mental réutilisable et une pierre angulaire fonctionnelle que vous pourrez appliquer à n'importe quel noyau numérique critique pour la sécurité.