ūüáßūüá∑ Por que estamos construindo Cardano? A Arte da Itera√ß√£o | Tradu√ß√£o parte 3 de 6 | Portugu√™s Brasileiro

A ARTE DA ITERAÇÃO
Criptomoedas s√£o protocolos implementados como software. Protocolos s√£o simplesmente conversas inteligentes entre os participantes. Em √ļltima an√°lise, o software √© a manipula√ß√£o de dados, com um objetivo. No entanto, a diferen√ßa entre software s√≥lido e confi√°vel, bem como protocolos √ļteis e seguros, e seu inverso √© completamente humana.

Um bom software precisa de responsabilidade, requisitos comerciais claros, processos repetíveis, testes completos e iteração incansável. Um bom software também precisa de desenvolvedores razoavelmente talentosos, com conhecimento específico do domínio suficiente para projetar adequadamente um sistema que possa resolver completamente qualquer problema que esteja tentando resolver.

Quanto aos protocolos √ļteis e seguros, especialmente aqueles que envolvem criptografia e sistemas distribu√≠dos, eles come√ßam em um processo mais acad√™mico e orientado a padr√Ķes. A revis√£o por pares, debates intermin√°veis ‚Äč‚Äče um conceito firme de trade-offs s√£o necess√°rios para garantir que um protocolo seja √ļtil. No entanto, esses fatores sozinhos n√£o s√£o suficientes, os protocolos precisam ser implementados e testados pelo uso na vida real.

O desafio √ļnico da ind√ļstria de criptomoedas √© que duas filosofias completamente diferentes s√£o mutiladas sem uma s√≠ntese hegeliana adequada. Nossa tese √© uma mentalidade de inicializa√ß√£o ‚Äúmova-se r√°pido e quebre as coisas‚ÄĚ, impulsionada pela juventude, gan√Ęncia e paix√£o. A ant√≠tese √© uma abordagem lenta, met√≥dica e academicamente orientada, motivada pelo desejo de solidificar as inova√ß√Ķes do nosso espa√ßo em um nicho agrad√°vel, com amplo financiamento e prest√≠gio.

O resultado é que muitas criptomoedas são totalmente especificadas em um white paper relevante apenas para um currículo ou apenas por código escrito às pressas. Nenhuma das dez principais criptomoedas atuais por capitalização de mercado é baseada em um protocolo revisado por pares. Nenhuma das dez principais criptomoedas atuais foi implementada a partir de uma especificação formal.

No entanto, bilh√Ķes de d√≥lares em valor est√£o em risco. Uma vez implantada, uma criptomoeda √© extremamente dif√≠cil de mudar. Como um usu√°rio sabe que est√° usando um sistema seguro? Como um usu√°rio sabe que as reivindica√ß√Ķes de marketing s√£o leg√≠timas? E se o protocolo proposto nunca conseguir as reivindica√ß√Ķes?

Essa falta de s√≠ntese e respeito ao processo √© uma das principais raz√Ķes pelas quais a IOHK queria construir o Cardano. Nossa esperan√ßa era desenvolver um projeto de refer√™ncia que servisse como exemplo de como fazer as coisas de maneira mais eficaz e honesta.

O objetivo n√£o √© propor uma maneira totalmente nova de desenvolver software e protocolos, mas reconhecer que j√° existem √≥timos softwares e protocolos e podemos imitar as condi√ß√Ķes que levaram √† sua cria√ß√£o. Segundo, tornar essas condi√ß√Ķes conhecidas publicamente e de c√≥digo aberto, se poss√≠vel, para que possam ser imitadas para o benef√≠cio de todo o campo.

FATOS E PARECERES
A outra preocupa√ß√£o √© onde os fatos terminam e a opini√£o come√ßa. Existem centenas de linguagens de programa√ß√£o, dezenas de paradigmas de desenvolvimento e mais de uma filosofia em gerenciamento de projetos. O mundo acad√™mico est√° cheio de seus pr√≥prios desafios decorrentes da dist√Ęncia das preocupa√ß√Ķes e da praticidade dos neg√≥cios.

Para Cardano, primeiro tentamos capturar defici√™ncias √≥bvias que podem ser universalmente aceitas como √ļteis do ponto de vista da engenharia. Por exemplo, criptografia e sistemas distribu√≠dos s√£o t√≥picos extraordinariamente envolvidos, com muitos exemplos de como m√£os ing√™nuas podem cometer erros terr√≠veis. Portanto, qualquer protocolo que exija discernimento desses dom√≠nios precisa ser projetado por um especialista reconhecido e submetido √† revis√£o por outros especialistas.

Ouroboros √© o nosso primeiro estudo de caso nesta √°rea. Foi projetado por uma equipe de criptografadores com um hist√≥rico de publica√ß√Ķes grande, diversificado e publicamente verific√°vel. Foi constru√≠do de acordo com o processo padr√£o de criptografia, com premissas de seguran√ßa, modelo advers√°rio e provas. Essas provas foram verificadas por submiss√£o √†s confer√™ncias e tamb√©m de forma independente por provas de computador escritas em Isabelle por uma equipe da Universidade de Cambridge.

No entanto, esse trabalho por si s√≥ n√£o oferece garantias de utilidade - apenas uma verifica√ß√£o rigorosa de um modelo de seguran√ßa, dadas algumas suposi√ß√Ķes. Para utilidade, √© preciso implementar e testar o protocolo. Nossos desenvolvedores fizeram isso tanto em Haskell quanto em Rust. Este trabalho revelou que era necess√°rio concentrar mais esfor√ßos no modelo de sincroniza√ß√£o, o que levou √† cria√ß√£o de Ouroboros Praos.

Essa arte de itera√ß√£o √© o que produz grandes protocolos, com cada etapa levando a novas li√ß√Ķes e um requisito para verificar novamente a corre√ß√£o da etapa anterior. √Č caro, demorado e √†s vezes realmente entediante, mas √© necess√°rio garantir que um protocolo seja projetado corretamente.

Os protocolos - especialmente aqueles a serem usados ‚Äč‚Äčpor bilh√Ķes de pessoas - n√£o t√™m vida curta e est√£o evoluindo rapidamente. Pelo contr√°rio, eles devem ser seguidos por anos a d√©cadas. Parece inteiramente razo√°vel que, antes de sobrecarregar o mundo com um novo sistema financeiro com o qual todos tenhamos que conviver nos pr√≥ximos 100 anos, desejemos exigir algum t√©dio e rigor de seus projetistas.

PECADOS FUNCIONAIS
Indo para um território mais opinativo, as ferramentas, linguagens e metodologias usadas no desenvolvimento de software são mais artefatos de providência religiosa do que realidade objetiva. O código fonte é como uma prosa escrita. Todo mundo tem uma opinião do que é bom - e o que está sendo comunicado às vezes é menos importante do que como ele é comunicado.

Devemos cometer o pecado de escolher um lado, aceitando que isso ser√° errado aos olhos de pelo menos uma pessoa. No entanto, h√° pelo menos um grande corpus de justificativa por tr√°s de nossa escolha.

Os protocolos que tornam Cardano possível estão sendo implementados em Haskell. A interface do usuário foi encapsulada em um fork do Electron que estamos chamando de Daedalus. Optamos por usar o modelo de arquitetura da Web sempre que possível e, para o nosso banco de dados, optamos por um paradigma de valor-chave usando o RocksDB.

Em um nível de componente, essa abstração significa que a manutenção é muito mais simples, melhor tecnologia pode ser substituída posteriormente com pouco esforço e que nossa pilha está parcialmente ligada aos esforços de desenvolvimento do GitHub e do Facebook.

O uso de um WebGuI nos permite alavancar o React e desenvolver recursos de front-end usando ferramentas conhecidas por centenas de milhares de desenvolvedores de JavaScript. Usar uma arquitetura da web significa que os componentes podem ser tratados como serviços e o modelo de segurança é sensato.

Escolher Haskell para o desenvolvimento do protocolo foi a escolha mais dif√≠cil. Mesmo no mundo funcional, existem amplas op√ß√Ķes. No lado mais flex√≠vel e impuro, existem linguagens como Clojure, Scala e F #, que se beneficiam das enormes bibliotecas dos ecossistemas Java e .Net, preservando alguns dos melhores aspectos da programa√ß√£o funcional.

Existem linguagens mais academicamente orientadas, como Agda e Idris, que t√™m uma estreita conex√£o com t√©cnicas que permitiriam uma forte verifica√ß√£o de corre√ß√£o. No entanto, elas n√£o possuem bibliotecas razo√°veis ‚Äč‚Äče t√™m uma experi√™ncia de desenvolvimento inferior.

Para Cardano, a escolha foi de Ocaml e Haskell. O Ocaml é um idioma maravilhoso, com uma ótima comunidade, boas ferramentas, experiência razoável em desenvolvimento e um grande legado no espaço formal de verificação por meio do Coq. Então, por que escolhemos Haskell?

POR QUE HASKELL?
Os protocolos que comp√Ķem Cardano s√£o distribu√≠dos, agrupados com criptografia e exigem um alto grau de toler√Ęncia a falhas. Nos melhores dias, ainda haver√° atores bizantinos, mensagens malformadas e clientes defeituosos, sem querer, causando algum tipo de confus√£o na rede.

Primeiro, quer√≠amos uma linguagem que possu√≠sse um sistema de tipos forte, onde pud√©ssemos usar facilmente ferramentas como Quickcheck e t√©cnicas mais elaboradas, como tipos de refinamento, mantendo uma expectativa razo√°vel de toler√Ęncia a falhas. Um modelo OTP do estilo Erlang satisfaz o √ļltimo, enquanto l√≠nguas como Haskell e Ocaml satisfazem o primeiro.

Com a introdução do Cloud Haskell, Haskell ganhou muitas das vantagens de Erlang sem se render. Além disso, a modularidade e a composição de Haskell nos permitiram usar uma biblioteca personalizada de menor peso chamada Time Warp for Cardano.

Segundo, as bibliotecas de Haskell evolu√≠ram bastante nos √ļltimos anos, gra√ßas ao extenso trabalho de entidades comerciais como Galois, FP Complete e Well-Type. Como conseq√ľ√™ncia, Haskell pode ser usado para escrever aplicativos de produ√ß√£o.

Terceiro, a rápida evolução do PureScript forneceu uma ponte muito necessária para o mundo JavaScript, semelhante ao que Clojurescript deu a Clojure. Esperamos que o PureScript seja especialmente importante quando o Cardano trabalha em um navegador e o desenvolvimento de carteiras móveis.

Quarto, com rela√ß√£o √† resolu√ß√£o de depend√™ncias, Haskell nos √ļltimos anos desfrutou de um esfor√ßo social e tecnol√≥gico significativo, liderado por tecn√≥logos como Michael Snoyman, por meio de uma plataforma chamada empilhamento que √© f√°cil de usar e √© bem suportada pelo FP Complete.

Em quinto lugar, al√©m da resolu√ß√£o adequada de depend√™ncias, pretendemos que nossas compila√ß√Ķes de software sejam reproduz√≠veis. Em outras palavras, com os mesmos valores de configura√ß√£o e vers√Ķes de depend√™ncia, ele deve produzir exatamente os mesmos artefatos de constru√ß√£o. Atrav√©s do empilhamento, usamos o NixOps para obter reprodutibilidade com grande sucesso.

Finalmente, o conjunto de talentos de desenvolvedores especializados em Haskell é razoavelmente grande - em comparação com seus pares - e bem treinado com a combinação certa de credenciais acadêmicas e do setor. Ele também atua como um filtro de competência, pois é incomum encontrar desenvolvedores experientes da Haskell sem conhecimento detalhado da ciência da computação.

ESPECIFICAÇÃO FORMAL E VERIFICAÇÃO
Uma for√ßa significativa do desenvolvimento de um protocolo usando um modelo de seguran√ßa comprovadamente correto √© que ele fornece um limite garantido de poder antag√īnico. √Č concedido um contrato que, desde que o protocolo seja seguido e as provas estejam corretas, o advers√°rio n√£o poder√° violar as propriedades de seguran√ßa reivindicadas.

Uma reflexão mais profunda torna a afirmação anterior ainda mais significativa. Os adversários podem ser arbitrariamente inteligentes e capazes. Dizer que eles são derrotados apenas através de um modelo matemático é extraordinário. E, claro, isso não é inteiramente verdade.

A realidade introduz fatores e circunst√Ęncias que impedem a utopia da pura seguran√ßa e do comportamento correto. Implementa√ß√Ķes podem estar erradas. O hardware pode introduzir vetores de ataque anteriormente n√£o considerados. O modelo de seguran√ßa pode ser insuficiente e n√£o estar em conformidade com o uso na vida real.

√Č necess√°rio um julgamento sobre quanta especifica√ß√£o, rigor e verifica√ß√£o s√£o exigidos para um protocolo. Por exemplo, empreendimentos como o projeto SeL4 Microkernel s√£o um excelente exemplo de um ataque √† ambiguidade, exigindo quase 200.000 linhas de c√≥digo Isabelle para verificar menos de 10.000 linhas de c√≥digo C. No entanto, um kernel de sistema operacional √© uma infraestrutura cr√≠tica que pode ser uma grave vulnerabilidade de seguran√ßa se n√£o for implementada adequadamente.

Todo software criptogr√°fico deve exigir o mesmo esfor√ßo herc√ļlea? Ou pode-se escolher um caminho menos vigoroso que produza resultados equivalentes? Tamb√©m importa se o protocolo √© perfeitamente implementado se o ambiente em que ele √© executado, √© notoriamente vulner√°vel, como no Windows XP?

Para Cardano, escolhemos o seguinte compromisso. Primeiro, devido à natureza complexa dos domínios da criptografia e da computação distribuída, as provas tendem a ser muito sutis, longas, complicadas e, às vezes, bastante técnicas. Isso implica que a verificação conduzida por humanos pode ser entediante e propensa a erros. Portanto, acreditamos que todas as provas significativas apresentadas em um white paper escrito para cobrir a infraestrutura principal precisam ser verificadas mecanicamente.

Segundo, para verificar o c√≥digo Haskell para que ele corresponda corretamente aos nossos white papers, podemos escolher entre duas op√ß√Ķes populares: interface com provadores SMT via LiquidHaskell e usando Isabelle / HOL.

Os solucionadores de SMT (teorias de m√≥dulo de satisfa√ß√£o) lidam com o problema de encontrar par√Ęmetros funcionais que satisfa√ßam uma equa√ß√£o ou inequa√ß√£o, ou mostrar alternativamente que tais par√Ęmetros n√£o existem. Conforme discutido por De Moura e Bj√łrner, os casos de uso do SMT s√£o variados, mas o ponto principal √© que essas t√©cnicas s√£o poderosas e podem reduzir drasticamente bugs e erros sem√Ęnticos.

Isabelle / HOL, por outro lado, √© uma ferramenta mais expressiva e diversificada que pode ser usada para especificar e verificar a implementa√ß√£o. Isabelle √© um solucionador de teoremas gen√©ricos que trabalha com constru√ß√Ķes l√≥gicas de ordem superior, capazes de representar conjuntos e outros objetos matem√°ticos a serem usados ‚Äč‚Äčem provas. A pr√≥pria Isabelle se integra ao Z3 SMT Prover para trabalhar com problemas que envolvem tais restri√ß√Ķes.

Ambas as abordagens fornecem valor e, portanto, decidimos adotá-las em etapas. As provas escritas humanas serão codificadas em Isabelle para verificar sua correção, satisfazendo, assim, nosso requisito de verificação da máquina. E pretendemos adicionar gradualmente Liquid Haskell a todo código de produção na implementação de Cardano ao longo de 2017 e 2018.

Como ponto final, a verifica√ß√£o formal √© t√£o boa quanto a especifica√ß√£o que est√° sendo verificada e os conjuntos de ferramentas dispon√≠veis. Uma das principais raz√Ķes para a escolha de Haskell √© que ela fornece o equil√≠brio certo de praticidade e teoria. As especifica√ß√Ķes derivadas dos white papers se parecem muito com o c√≥digo Haskell, e conectar os dois √© consideravelmente mais f√°cil do que faz√™-lo com uma linguagem imperativa.

Ainda h√° uma enorme dificuldade em capturar uma especifica√ß√£o adequada e tamb√©m atualiz√°-la quando altera√ß√Ķes como atualiza√ß√Ķes, corre√ß√Ķes de bugs e outras preocupa√ß√Ķes precisam ser feitas; no entanto, essa realidade n√£o diminui de forma alguma o valor geral. Se algu√©m tiver problemas para construir uma base com seguran√ßa comprovada, a implementa√ß√£o deve ser o que foi realmente proposto no papel.

TRANSPARÊNCIA
Uma pergunta final ao discutir a ci√™ncia e a engenharia do desenvolvimento de uma criptomoeda √© como abordar a transpar√™ncia. As decis√Ķes de design n√£o s√£o booleanas e et√©reas, chegando aos desenvolvedores em sonhos e subitamente se tornando um canh√£o. Eles s√£o derivados da experi√™ncia, debate e li√ß√Ķes aprendidas com erros anteriores.

O desafio √© que um processo de desenvolvimento totalmente transparente possa influenciar a discuss√£o a se tornar mais teatral do que baseada em evid√™ncias. Egos, tentativas de conquistar uma comunidade e medo de parecer est√ļpido podem for√ßar as conversas a se tornarem est√©reis e contraproducentes.

Al√©m disso, pessoas de fora poderiam tentar cooptar a conversa em um esfor√ßo para for√ßar sua tangente espec√≠fica a se tornar o √ļnico t√≥pico relevante. Todo mundo tem uma vaca sagrada.

Então, como equilibrar a necessidade de um processo de desenvolvimento transparente, devido à comunidade que confiou o progresso a um conjunto de desenvolvedores principais, com a necessidade de liberdade de expressão sem medo?

Com Cardano, decidimos adotar um processo orientado por padr√Ķes com supervis√£o direta. A comunidade precisa saber que a ci√™ncia e o c√≥digo s√£o bem pensados, verificados e realmente resolvem o que os desenvolvedores afirmam que fazem. Para esse fim, a revis√£o por pares deve satisfazer completamente o componente cient√≠fico, uma vez que foi projetado especificamente para esse fim e nos deu o mundo moderno.

Para código, este tópico é um pouco mais opinativo. Para Cardano, optamos por confiar a Fundação Cardano para servir como auditor final do trabalho da IOHK. Em particular, são encarregados dos seguintes deveres:

  1. Revisão regular do código fonte contido no Cardano GitHub para verificar a qualidade, a cobertura dos testes, os comentários adequados e a integridade

  2. Revisão de toda a documentação do Cardano para correção e utilidade

  3. Verificando as alega√ß√Ķes de que os protocolos produzidos pelos cientistas s√£o totalmente implementados

Para realizar essa tarefa, a IOHK enviará relatórios regulares e oportunos à Fundação - e seus designados - para revisão. A Fundação, por sua vez, divulgará um relatório de supervisão de desenvolvimento para a comunidade Cardano pelo menos trimestralmente.

Esse primeiro esfor√ßo visa iniciar uma conversa mais ampla sobre como um projeto descentralizado alcan√ßa a responsabilidade. A supervis√£o do desenvolvimento de terceiros confi√°veis ‚Äč‚Äč√© uma ferramenta poderosa para garantir que os desenvolvedores estejam no caminho certo, mas n√£o √© suficiente para garantir completamente que o projeto sempre ser√° entregue.

Por esse motivo, depois que o tesouro for integrado √† CSL, a Funda√ß√£o incentivar√° equipes de desenvolvimento adicionais a construir clientes alternativos com base nas especifica√ß√Ķes formais desenvolvidas em conjunto com a IOHK. A diversidade de desenvolvimento tem sido uma √≥tima t√©cnica usada pelo projeto Ethereum para evitar a forma√ß√£o de uma monocultura em torno de um √ļnico conjunto de id√©ias ou desenvolvedores.

No que diz respeito √†s especifica√ß√Ķes, existe um vasto conhecimento a ser obtido com o processo de padr√Ķes seguido pelo WC3 e pelo IETF. Por fim, cada protocolo que o Cardano integra requer uma especifica√ß√£o independente do trabalho acad√™mico ou do c√≥digo-fonte. Em vez disso, ele precisa estar em um formato adequado, como um RFC.

Um dos princ√≠pios fundamentais da Cardano Foundation √© atuar como √≥rg√£o de padr√Ķes especificamente para os protocolos Cardano e hospedar conversas para atualizar, adicionar ou alterar padr√Ķes relevantes para o Cardano. Se a Internet (um produto de padr√Ķes) atrav√©s da IETF pode chegar a um consenso sobre quais protocolos principais devem ser usados, √© perfeitamente razo√°vel supor que um organismo dedicado possa facilitar o mesmo resultado.

Como observa√ß√£o final, √© interessante explorar a mudan√ßa dessas discuss√Ķes para uma entidade descentralizada hospedada em uma blockchain. Esse conceito √© chamado de organiza√ß√£o aut√īnoma descentralizada (DAO) e o trabalho preliminar est√° em andamento nessa √°rea. A IOHK desenvolver√° um modelo de DAO de refer√™ncia para entidades que fazem interface com Cardano, se desejado, e √© uma prerrogativa da Cardano Foundation decidir se deve adot√°-lo sob seu mandato de padr√Ķes.

Notas de rodapé

18: Consulte coinmarketcap.com para obter uma lista abrangente por capitalização de mercado.

19: Ethereum tem uma especifica√ß√£o semi-formal conhecida como Livro Amarelo; no entanto, a sem√Ęntica do EVM n√£o √© totalmente especificada nem √© suficiente para uma implementa√ß√£o completa do protocolo.

20: Artigo aceito n√ļmero 71 da Confer√™ncia anual de criptografia da IACR na Calif√≥rnia.

21: Por Kawin Worrasangasilpa, sob a supervis√£o do professor Lawrence Paulson.

22: Após uma tangente de uma estaca de leviandade, deve-se assistir à discussão do professor Halmo sobre como escrever um livro de matemática.

23: Adicionando a esse ponto, o IOHK realmente tem um projeto em execu√ß√£o no Ocami chamado Qeditas, que herdamos do pseud√īnimo de Bill White.

24: Bryan O’Sullivan oferece uma boa conversa sobre o uso industrial de Haskell aqui.

Fonte Original: https://cardano.org/why/science-and-engineering/

Traduzido por Bosco Cardosco @boscokim || Telegram @boscox
Parte 4: ūüáßūüá∑ Por que estamos construindo Cardano? Interoperabilidade | Tradu√ß√£o parte 4 de 6 | Portugu√™s Brasileiro

1 Like