Em sistemas de computação com aplicações sensíveis (área financeira, lançamento de um foguete) busca-se por códigos comprovadamente livres de falhas. O modelo tradicional para assegurar a qualidade do software se baseia na detecção de falhas em tempo de execução através da criação e execução de testes automatizados. Este método, por sua natureza, garante apenas que especificamente o que foi testado funciona conforme verificado pelos testes. Como o número de testes é finito, tais técnicas não raramente são combinadas com a avaliação da cobertura de código. Ainda assim, este método não é capaz de provar que não há falhas assim como não impede que códigos incorretos sejam escritos. Ademais, para qualquer software de tamanho razoável a complexidade ciclomática para que todos os caminhos de execução sejam verificados torna a escrita de testes de maneira manual proibitivamente complexa.
Um modelo complementar é o da utilização de tipos e funções com restrições de tal forma a maximizar a localização de erros em tempo de compilação, evitando que eles ocorram em tempo de execução. Esta abordagem evita a escrita de diversos testes automatizados que, por definição, perdem o seu sentido em uma linguagem com tipagem mais restritiva já que o compilador ou prova que tais situações são impossíveis ou emite um erro de compilação.
Nesta série de posts, descrevemos os avanços mais recentes em programação funcional, programação no nível dos tipos e linguagens com tipos dependentes.
Uma playlist com aulas gravadas sobre todos os tópicos abordados neste material pode ser vista aqui.