Diretor de métodos formais, Philipp Kant explica a nossa metodologia para construir software com flexibilidade e precisão.
Forma e função
IOHK está a construir um sistema operativo financeiro e social. Esta tarefa enorme requer não só, iterações rápidas, mas também precisão absoluta. É por isso que a IOHK escolheu combinar a velocidade de desenvolvimento ágil com código de elevada garantia e métodos formais. Fundir a flexibilidade com a formalidade levou os nossos engenheiros a serem pioneiros nesta filosofia de desenvolvimento moderna.
A IOHK acredita firmemente na investigação, métodos formais, programação funcional cuja construção é realizado de forma rigorosa. Enquanto competidor no desenvolvimento da indústria de blockchain temos que de forma consistente demonstrar progresso e criação de valor para a comunidade global das nossas partes interessadas. Isto significa que não podemos comprometer a robustez ou na velocidade de desenvolvimento e flexibilidade. Num ambiente constantemente em mutação isto é um desafio, por isso os nossos programadores têm que encontrar um equilíbrio.
Agilidade contra formalidade
As normas de desenvolvimento de tecnologia no mundo das start-up tem sido a de criar produtos de viabilidade mínima de forma rápida e depois iterar de forma contínua até atingir o mercado das massas. Isto é conhecido pelo processo ágil. Trata-se de uma forma fantástica para mostrar que um projeto pode avançar enquanto se constrói um produto totalmente funcional. Contudo, a metodologia ágil assume que haverá erros e fraquezas em cada passo do desenvolvimento que pode ser eliminados posteriormente. Isto pode acontece se não houver valor em risco - contudo, com moedas virtuais, existe uma quantidade enorme de moeda e confiança de partes interessadas que confiam nessa linha.
Construir um ativo digital numa blockchain fornece vários desafios a ultrapassar em termos de organizar o processo de desenvolvimento. Enquanto uma moeda baseada na prova de participação, Cardano é um sistema distribuído num ambiente com adversários onde o desempenho é crítico. O protocolo tem que manter a segurança face a atores maliciosos que tentam sabotagem. Isto significa que ninguém pode correr o risco de construir rapidamente e lidar com os problemas mais tarde.
Confiança é essencial para uma moeda ser aceite e a retidão das evidências são um importante passo para aumentar a veracidade do sistema. É por isso que código, não só tem que ser correto, mas também deve haver evidências da sua retidão, tais como testes significativos e extensos e evidências matemáticas. Numa indústria jovem como as criptomoedas, engenheiros da IOHK têm que antecipar novas características enquanto garantem ao mesmo tempo a retidão estabelecida na versão inicial. A plataforma pode apenas escalar globalmente se for capaz de crescer enquanto mantiver a segurança e utilidade para todos. É por isso que os programadores de Cardano simplificaram a metodologia, combinando uma variedade de ferramentas desde testes baseado em propriedades até evidências verificáveis por máquinas para assegurar software de elevada garantia mesmo na presença da mudança de requisitos.
Investigação até ao código
A metodologia começa com a investigação científica. Até à data, a IOHK publicou mais de 60 artigos científicos que têm contribuído para a criação da plataforma. Cada artigo examina um aspeto crítico da tecnologia blockchain dos princípios fundamentais. Como é que obtemos o consenso de forma descentralizada? Como é que um contrato inteligente é concebido? Qual a estrutura de recompensas para incentivar um bom comportamento? Investigadores da IOHK examina estas questões e submetem as suas respostas a jornais e conferências científicos. Estes artigos contêm evidências que têm que passar uma rigorosa revisão de pares. Depois, para garantir que a qualidade do nosso software faz justiça à investigação, é desenvolvido usando métodos formais.
Na sua essência, significa que engenheiros da IOHK especificam o que o código deve fazer em termos matemáticos. Assim, podem assegurar que quando o código é executado contém as propriedades desejadas conforme a sua conceção. O código é escrito em Haskell, uma linguagem de programação funcional de elevada garantia com um sistema de tipos robusta. Enquanto que Haskell é uma ferramenta fantástica para implementar software fiável, contudo não é infalível, assim o código continua a precisar de ser testado. Uma forma fantástica para escrever testes é QuickCheck, que permite a programadores constatarem propriedades de estado que têm que sempre ser assegurados num programa. QuickCheck gera casos de teste e pesquisa pequenos contraexemplos que violam estas propriedades.
Código que interage com o mundo externo, em particular aplicações de rede, pode ser difícil encontrar pequenos contraexemplos. Isto é porque a ordem de execução não é determinística: pode mudar todas as vezes que o software for executado. O mesmo código pode ser executado centenas de vezes e falhar apenas uma vez. Podemos dar a volta a isto com simulações com ordens de execução determinística. Executar testes em simulação permite-nos encontrar de forma fiável e corrigir classes de erros durante os testes que caso contrário apenas ocorreriam de forma aleatória em produção.
Colmatar a lacuna
Para ter uma imagem da metodologia de desenvolvimento empregue por Cardano, consideremos a metáfora de construir uma ponte. Quando um engenheiro civil construi uma ponte, uma grande porção do tempo é gasto por trás da secretária. O engenheiro civil planeia a conceção, calcula com estatísticas e levantamentos de ordens geográficas. Durante esse período, nada acontece no local de construção. Um observador seria incapaz de ver algum progresso realizado. Para construir pontes, esta é a abordagem correta. Se o planeamento não for rigoroso, é difícil e dispendioso corrigir problemas numa fase posterior. Em última instância o resultado seria uma ponte atrasada a um custo mais dispendioso ou uma que falha por completo. A falta de visibilidade do progresso é um bom preço a pagar para obter uma ponte funcional e segura.
Quando construímos software, fazer alterações em fases avançadas é muito mais fácil do que durante a construção. Isto é o que permite a abordagem de desenvolvimento ágil. Se um programador ágil for construir uma ponte, iriam construir um pilar num sprint rápido e depois outro no próximo sprint. O espaço entre os pilares seria fechado num último sprint e, se tudo resistir, os programadores iriam adicionar mais um sprint para corrigir os problemas que, entretanto, teriam aparecido. Enquanto o progresso seria demonstrado no local de construção , o produto final teria provavelmente que lidar com um elevado número de problemas incorporados. Isto cria trabalho de limpeza no final do projeto que poderia ser evitado através de melhor planeamento nas fases iniciais. Mais, o produto de viabilidade mínima seria dado a um pequeno grupo de pessoas para testes iniciais com a expectativa de que falharia de modo a alertar programadores aos erros.
Quando ouvem as palavras “métodos formais” muitas pessoas no desenvolvimento de software pensam na abordagem referido na engenharia civil que é denominado “waterfall” e genericamente evitado. Isto é comum, mas uma interpretação infeliz. De facto, usar apropriadas técnicas formais permite-nos ter e comer o bolo ao mesmo tempo: para termos uma conceção geral (uma conceção deliberada, e não acidental resultado do encaixe de muitas peças desenvolvidas de forma individual em sprints), para mostrar progresso contínuo, e reter a capacidade de reagir a requisitos que alteram.
A técnica chave empregue pelos programadores da IOHK são as especificações executáveis. Trata-se de conceções de elevado nível, que abstraem todos os detalhes mais minuciosos, escrito numa linguagem que um computador pode compreender e executar. Especificações executáveis podem ser utilizados como protótipos para mostrar progresso, obter comentários dos utilizadores e testar pressupostos. Em cima disso, detalhes mais minuciosos podem ser adicionados via refinamentos sucessivos. Os nossos programadores podem construir uma ponte para resolver os maiores problemas primeiro e depois adicionar pilar para reforçá-la mais tarde. Num sistema de software, os pilares seriam características como gravar dados para o disco, ou usar algoritmos de maior desempenho, que são necessários para o produto final, mas que não são essenciais para demonstrar as funcionalidades mais abrangentes.
Ao usar especificações executáveis obtemos os benefícios de planeamento adequado sem sacrificar a flexibilidade. Os programadores da IOHK podem fixar o sistema ao que pretendem que seja numa escala maior e depois implementar componentes adequados conforme sejam necessários. Testes contínuos garantem que cada componente se encaixa na conceção global. Isto ajuda a prevenir problemas que são comuns numa abordagem de integração posterior. Com esta metodologia, obtemos o melhor de ambos os mundos: podemos usar conceção de cima para baixo (evitando desafio de integrações posteriores, tendo bom pulso sobre a conceção em todos os instantes) e ter código em desenvolvimento cedo (demonstrando progresso e permitindo realizar testes e receber comentários durante todo o processo).
À prova do futuro
Em última instância, o método de construção deve ser determinado por aquilo que está a ser construído. A IOHK está a construir um sistema operativo financeiro e social global que requer rigor e velocidade. Formal vs. ágil é uma falsa dicotomia. Em vez disso, estamos a continuar o desenvolvimento da nossa metodologia que fude o melhor de ambas as abordagens: técnicas formais dentro de um enquadramento de entrega ágil com código robusto e de elevada garantia na qual se pode construir todo o nosso futuro.