Desenvolvedor formaliza kernel da linguagem Bend e oferece recompensa
Victor Taelin formalizou o kernel da linguagem Bend e instituiu um prêmio de US$ 10 mil para quem encontrar falhas no sistema.
||
27/09 às 13:40
Pontos principais
- O kernel de prova do Bend foi verificado formalmente com a linguagem Lean.
- Foi lançado um desafio de US$ 10 mil para quem provar a existência de falsidades no sistema.
- O novo comando --verdict permite compilar arquivos para o BendTT, um kernel de prova verificado.
- A atualização 2.0.32 traz melhorias no backend JS e suporte a arrays compartilhados.
O desenvolvedor Victor Taelin anunciou a formalização do kernel de prova da linguagem Bend, que agora utiliza o BendTT, um kernel minimalista verificado através da linguagem Lean. Como parte do lançamento da versão 2.0.32, foi instituída uma recompensa de US$ 10 mil para qualquer pessoa que consiga provar a existência de falsidades no sistema.
A atualização também introduziu o comando --verdict para compilação e implementou melhorias técnicas no backend JS. Entre as mudanças, destacam-se a redução no tempo de inicialização de binários e a adição de suporte a arrays compartilhados.
Comentários
Carregando comentários...
