A observação é sobre um uso específico do Coq, a formalização da teoria da linguagem de programação.
Vamos primeiro esclarecer a distinção entre sintético e analítico :
Numa abordagem sintética de um assunto, dizemos que existem coisas cujas propriedades e estrutura básicas são postuladas de uma maneira ou de outra. Em seguida, estudamos essas coisas confiando apenas nas propriedades e na estrutura postuladas.
Numa abordagem analítica de um assunto, descobrimos que existem certas coisas. Para aprender mais sobre eles, nós os separamos, estudamos como eles são feitos e os analisamos. Desta forma, descobrimos suas propriedades e estrutura.
Como alguém estudaria uma linguagem de programação dessas duas maneiras?
Sinteticamente, postularíamos as partes constituintes da linguagem (existem termos, existem tipos), sua estrutura básica (essas são as formas de construir termos) e propriedades básicas. Não perguntamos de que são feitos os termos e o tipo, ou se os termos são árvores ou seqüências de caracteres, ou se a coleção de tipos é construída de uma maneira específica.
Analiticamente, começaríamos com uma configuração matemática que nos permite fazer muitas coisas, como usar definições indutivas para construir objetos matemáticos. Construímos termos e tipos como conjuntos ou tipos específicos definidos indutivamente. Então estudaríamos sua estrutura, como podemos transformá-los, etc.
Deve ficar claro que Coq é do tipo analítico. Ao implementar uma linguagem de programação no Coq, você define tipos indutivos de termos e tipos. Em seguida, você os analisa usando indução, define semântica operacional como uma função recursiva na sintaxe dos termos, etc.
Por outro lado, Twelf é do tipo sintético. Postulamos que existe um tipo de termos e um tipo de tipos, mas não dizemos a Twelf que esses são tipos indutivos (não há como dizer isso em Twelf). Definimos semântica operacional, fornecendo regras básicas de transição. Não há menção de funções definidas recursivamente (não há como definir funções no Twelf), apenas confiamos nos postulados que escrevemos.
Você deve comparar a situação acima com a geometria planar. A abordagem de Hilbert à geometria é sintética (mas suas idéias estão enraizadas em Euclides), as de Descartes são analíticas. A geometria analítica é assim chamada porque uma linha não é um conceito primitivo: possui uma estrutura interna, ou seja, é um conjunto de pontos.
