Discussion autour d’un système de typage

Discussion autour d’un système de typage. Écrire des programmes corrects et prouver leur correction est une tâche pleine de défis. Pour appréhender ce problème, les langages de programmation modernes sont équipés d’un système de typage. Les types sont des constructions syntaxiques semblables à des formules logiques qui permettent aux machines de vérifier automatiquement si les programmes sont bien typés et qu'ils ne produisent pas une certaine classe d’erreurs à l’exécution. Le premier système de typage a été proposé en 1908 par Russel très précisément pour éviter d’écrire des expressions qui n’auraient aucun sens, autrement dit des paradoxes.