O que os designers de linguagem fazem para decidir ou provar que um recurso específico funciona corretamente?

Estou interessado em design de linguagem e, em geral, posso raciocinar facilmente sobre recursos amplamente conhecidos (por exemplo, herança, polimorfismo, delegados, lambdas, capturas, coleta de lixo, exceções, genéricos, variação, reflexão etc.), suas interações em um linguagem específica, as formas como elas podem ser implementadas, suas limitações etc.

Nos últimos meses, comecei a ler sobre o Rust, que possui um sistema de propriedade que garante a segurança da memória e o gerenciamento determinístico de recursos, forçando a vida útil do objeto a ser estaticamente verificável. Da perspectiva de um usuário comum da linguagem, eu pude entender o sistema quase imediatamente.

Da perspectiva de um designer de linguagem, no entanto, levei um tempo para perceber por que as coisas no Rust são exatamente do jeito que são. Eu não conseguia entender imediatamente o raciocínio por trás de algumas restrições do sistema de propriedade, até me forçar a apresentar casos que violariam a integridade de um sistema se ele não tivesse esses aspectos.

Minha principal pergunta não tem nada a ver com o Rust e sua propriedade especificamente - mas fique à vontade para usá-lo como exemplo em seus comentários / respostas, se necessário.

Quando os designers de linguagem projetam um novo recurso, que metodologia ou processo eles usam para decidir se o recurso funciona corretamente?

Por "novo", quero dizer que não é algo que já foi testado em idiomas existentes (e, portanto, a maior parte do trabalho foi realizada por outros designers). Por "funciona corretamente", quero dizer que o recurso resolve o problema pretendido corretamente e é razoavelmente à prova de balas. Por "razoavelmente à prova de balas", quero dizer que nenhum código pode ser escrito no idioma ou em um subconjunto específico do idioma (por exemplo, um subconjunto sem código "não seguro") que viole a integridade do recurso.

• É um processo de tentativa e erro, no sentido de que você cria uma forma simples do recurso, tenta encontrar maneiras de violá-lo, corrige-o se violá-lo com sucesso e repita? E então, quando você não consegue pensar em outras possíveis violações, espera que não haja mais nada e encerra o dia?

• Ou existe uma maneira formal de realmente provar (no sentido matemático da palavra) que seu recurso funciona e depois usá-lo para obter o recurso certo (ou quase sempre) com confiança desde o início?

(Devo mencionar que tenho formação em engenharia, não ciência da computação. Portanto, se estiver faltando algo que seria óbvio para o pessoal da CS, fique à vontade para apontar.)

Estou tendo problemas para encontrar a referência exata no momento, mas há algum tempo assisti a vários vídeos de Simon Peyton Jones , que foi um dos principais colaboradores do design de Haskell. Ele é um excelente palestrante sobre teoria de tipos, design de linguagem e similares, a propósito, e tem muitos vídeos disponíveis gratuitamente no youtube.

Haskell tem uma representação intermediária que é essencialmente o cálculo lambda aumentado com algumas coisas simples para facilitar o trabalho. O cálculo Lambda tem sido usado e comprovado, já que um computador era apenas uma pessoa que calculava as coisas. Um ponto interessante que Simon Peyton Jones costuma enfatizar é que, sempre que eles fazem algo louco e louco com a linguagem, ele sabe que é fundamentalmente bom quando eventualmente se reduz a essa linguagem intermediária.

Outros idiomas não são tão rigorosos, favorecendo a facilidade de uso ou implementação. Eles fazem o mesmo que outros programadores fazem para obter código de alta qualidade: siga boas práticas de codificação e teste-o até a morte. Um recurso como a semântica de propriedade de Rust, tenho certeza, recebe muitas análises e testes formais para encontrar casos esquecidos. Muitas vezes, recursos como esse começam como uma tese de graduação de alguém.

Portanto, para o design da linguagem , existem provas (ou bugs). Por exemplo, digite sistemas. Tipos e linguagens de programação é o livro canônico que descreve os sistemas de tipos e se concentra em provar a correção e a integridade do sistema de tipos. As gramáticas têm análises semelhantes e os algoritmos (como o sistema de propriedade que você descreve) têm os seus.

Para implementação de linguagem , é código como qualquer outro. Você escreve testes de unidade. Você escreve testes de integração. Você faz revisões de código.

A única coisa que torna as línguas especiais é que elas são (quase sempre) infinitas. Você literalmente não pode testar todas as entradas. E (idealmente) eles são usados ​​por toneladas de pessoas, fazendo coisas estranhas e interessantes, de modo que qualquer bug no idioma será encontrado eventualmente.

Praticamente , relativamente poucos idiomas usam provas para verificar sua funcionalidade e terminam com uma mistura das opções mencionadas.

A primeira e mais difícil coisa que um designer de idiomas deve cuidar ao introduzir novos recursos é manter seu idioma consistente:

• como ele pode ser integrado à gramática da linguagem sem quebrar o código existente (isso pode ser matematicamente comprovado)
• como ele se relaciona com os recursos existentes (por exemplo, se você tiver arrays fixos indexados 0..n-1, não introduzirá um novo recurso de array variável indexado 1..n) (essa é a parte artística do design)
• como o recurso pode ser implementado em toda a cadeia de ferramentas para que o novo recurso possa ser absorvido pelo ecossistema, pelos fabricantes de ferramentas e pelos programadores (a viabilidade pode ser demonstrada com uma prova de conceito, mas a implementação completa é uma abordagem semelhante à programação)

Para orientar nesse assunto, um designer depende de um conjunto de regras e princípios de design. Essa abordagem é muito bem descrita em " O design e a evolução do C ++ ", de Bjarne Stroustrup , um dos raros livros dedicados ao design de linguagem. O que é muito interessante é ver que os idiomas raramente são projetados no vácuo, e o designer também olha como seus idiomas implementaram recursos semelhantes. Outra fonte (online e gratuita) são os princípios de design para a linguagem java .

Se você observar os procedimentos públicos dos comitês de padronização, verá que é mais um processo de erro de tentativa. Aqui um exemplo no módulo C ++, um conceito totalmente novo a ser introduzido na próxima versão da linguagem. E aqui uma análise elaborada após algumas mudanças de idioma , para avaliar seu sucesso. E aqui o Java Community Process para definir novas especificações Java, como uma nova API . Você verá que este trabalho é realizado por vários especialistas que elaboram de forma criativa um documento conceitual e uma primeira proposta. Em seguida, essas propostas são analisadas por uma comunidade / comitê maior, que pode alterar a proposta para garantir um maior grau de consistência.

Como testar os recursos da linguagem de programação? É uma pergunta muito boa, e não tenho certeza de que o estado da arte esteja à altura do trabalho.

Cada novo recurso pode interagir com todos os outros recursos. (Isso afeta o idioma, documentos, compiladores, mensagens de erro, IDEs, bibliotecas etc.) Os recursos são combinados para abrir uma brecha? Para criar casos extremos desagradáveis?

Até designers de linguagem muito inteligentes, trabalhando duro para manter a solidez do tipo, descobrem violações como esse bug do Rust . O sistema de tipos da Rust não é tão óbvio para mim, mas acho que, nesse caso, ter o sistema de tipos rastrear as vidas úteis dos valores significa "sub-tipificação" (sub-faixas) da vida em conflito com as expectativas de subtipagem, coerção, referências e mutabilidade comuns, criando uma brecha na staticvida ref pode apontar para um valor alocado pela pilha e depois se tornar uma referência pendente.

Por "funciona corretamente", quero dizer que o recurso resolve o problema pretendido corretamente e é razoavelmente à prova de balas.

Para idiomas destinados a serem idiomas de produção , isto é, usados ​​por muitos programadores para criar software de produção confiável, "funciona corretamente" deve significar resolver ainda mais o problema pretendido corretamente para o público-alvo.

Em outras palavras, a usabilidade é tão importante para o design de linguagem quanto para outros tipos de design. Isso envolve (1) design de usabilidade (por exemplo, conhecer seu público) e (2) teste de usabilidade.

Um exemplo de artigo sobre este tópico é "Os programadores também são pessoas, a linguagem de programação e os designers de API podem aprender muito com o campo do design de fatores humanos".

Um exemplo de pergunta SE sobre este tópico é: A sintaxe de qualquer linguagem de programação foi testada quanto à usabilidade?

Um exemplo de teste de usabilidade considerou estender um recurso de iteração de lista (não lembro qual idioma) para pegar várias listas. As pessoas esperavam que ele repetisse as listas em paralelo ou através do produto cruzado? Os designers de linguagem ficaram surpresos com os resultados dos testes de usabilidade.

Idiomas como Smalltalk, Python e Dart foram projetados com ênfase na usabilidade. Claramente Haskell não era.