Le langage formel d'une discipline scientifique est un langage obéissant à une syntaxe formelle stricte, servant à exposer des énoncés de manière précise, si possible concise et sans ambiguïté ; ce qui l'oppose au langage naturel.
Compréhension à l'aide d'ordinateurs
Dès le début de l'informatique les chercheurs ont développé des outils d'aide à la traduction des langages, afin de passer du format externe au format interne de l'ordinateur. Les outils les plus connus sont Lex et Yacc. D'autres chercheurs ont défini la sémantique des langages de programmation.
Dans l'histoire des mathématiques et des sciences
Avant le XX siècle
Les mathématiques existent depuis l'Antiquité mais la manière de les exprimer a énormément évolué.
Comme pour toute discipline, le langage de la discipline ne préexiste pas à la discipline elle-même. Il a donc fallu utiliser des langues qui n'ont pas été construites pour les mathématiques, qui peu à peu se sont enrichies d'un jargon spécifique.
Ainsi, bien des énoncés mathématiques anciens nous paraissent aujourd'hui avoir une formulation plutôt alambiquée, surchargée de périphrases quand il n'existe pas de mots pour désigner certains concepts.
Le jargon s'est donc enrichi au cours des siècles et continue encore d'évoluer.
Parallèlement à ce phénomène, s'est progressivement formé le langage formel qui est devenu celui que nous connaissons, le langage naturel ne s'étant montré ni assez précis ni assez concis.
Leibniz fut l'un des premiers à imaginer construire un langage formel, sous le nom de caractéristique universelle, qui pourrait permettre de réduire toutes les obscurités et équivocités du langage naturel. Un projet d'éclaircissement du langage naturel avait déjà été formulé par Hobbes et Locke, mais Leibniz l'a porté à un niveau d'universalité inédit. Bien qu'il échouât dans ce projet, celui-ci fut repris, et a été l'un des objectifs principaux du Cercle de Vienne, au début du XX siècle.
Au XX siècle
Au début du XX siècle, le mathématicien David Hilbert, et avec lui, les formalistes pensaient pouvoir unifier les mathématiques grâce à une axiomatisation générale et à l'usage d'un langage formel commun.
Cette vision des mathématiques fut mise à mal en 1931 lorsque le logicien Kurt Gödel annonça son célèbre théorème d'incomplétude qui démontre que dans tout système formel contenant l'arithmétique, il existe au moins une proposition indécidable.
Pour revenir aux langages formels, la conséquence de ce théorème est la suivante : étant donné un langage formel, ses axiomes, et son système de déduction formel capables d'exprimer l'arithmétique, on peut énoncer une proposition de ce langage qui ne peut pas être prouvée dans ce système, mais dont la négation non plus ne peut l'être. On aura beau formaliser les mathématiques, on trouvera toujours un énoncé formel dont la démonstration oblige à quitter ou élargir ce formalisme en ajoutant de nouveaux axiomes, ce qui introduira immanquablement de nouveaux énoncés indécidables. Ainsi l'approche formaliste, qui reste pourtant valable, a désormais des limites connues.
Dans la seconde moitié du XX siècle, l'avènement des ordinateurs et de l'informatique a donné une place particulière aux langages formels en tant qu'outils et en tant qu'objets d'étude, ce qui était relativement nouveau.
Aujourd'hui (début du XXI siècle)
Les traités de mathématiques utilisent à la fois langage formel et langage naturel. Le langage formel est réservé aux passages techniques et aux énoncés suffisamment simples pour ne pas nécessiter d'amples explications, et les résultats importants sont souvent explicités à la fois en langage formel et naturel.
Le langage formel mathématique contemporain est décrit dans cet article.