41: Lean e Verificação de Software, com Leonardo de Moura (AWS)

Vídeo no YouTube

Episódio do podcast

Todas as plataformas

Lean e Verificação de Software, com Leonardo de Moura (AWS)

Spotify

Spotify para Podcasters

Resumo

Neste episódio do Fronteiras da Engenharia de Software, Adolfo Neto entrevista o pesquisador Leonardo de Moura, Senior Principal Applied Scientist no Grupo de Raciocínio Automatizado na AWS e Chief Architect da Lean FRO. Leonardo é reconhecido por diversas contribuições, entre elas o desenvolvimento do Z3, um SMT Solver, e da Lean, que é ao mesmo tempo uma linguagem de programação funcional e um provador de teoremas.

A entrevista é dividida em partes, começando com a apresentação de Leonardo e de sua trajetória desde o doutorado na PUC-Rio até sua posição atual na AWS. Em seguida, Leonardo  explora os conceitos fundamentais sobre verificação de software e como provadores de teoremas, como o Z3, são aplicados nesse contexto.

A terceira parte destaca a evolução do Lean, inicialmente uma ferramenta para matemáticos, para se tornar uma linguagem de programação funcional (Lean 4). Leonardo compartilha insights sobre o sucesso do Lean, sua comunidade ativa e as possibilidades que a linguagem oferece para desenvolvimento e verificação de software.

Dentro do enfoque em Lean, são abordados temas como a mudança para ser uma linguagem de programação funcional, a base em teoria dos tipos dependentes e as potenciais aplicações em pesquisa e desenvolvimento de software. Perguntas do Twitter sobre o uso do Lean fora do meio acadêmico e a Teoria da Homotopia são discutidas, assim como as perspectivas de pesquisa com o Lean 4.

A quarta parte explora temas diversos, como a participação de Lean na Rinha de Backend, onde uma implementação em Lean se destacou, e a criação da Lean FRO, uma organização focada em pesquisa do Lean. Também são discutidos os avanços em IA e como o Lean pode se beneficiar dessas tecnologias.

Na parte final, Adolfo pergunta a Leonardo sobre a próxima fronteira da engenharia de software, proporcionando uma visão do que pode vir a moldar o futuro da área. O episódio encerra com agradecimentos aos ouvintes e a promessa de retornar com mais discussões no próximo episódio do Fronteiras da Engenharia de Software.

Sobre Leonardo de Moura:

• Página https://leodemoura.github.io/ 

• Escavador https://www.escavador.com/sobre/7442280/leonardo-mendonca-de-moura 

• Scholar https://scholar.google.com/citations?user=CwazDKgAAAAJ&hl=pt-BR&oi=ao

• DBLP https://dblp.org/pid/d/LeonardoMdeMoura.html 

• Linkedin https://www.linkedin.com/in/leonardo-de-moura-26a27b5/ 

• GitHub https://github.com/leodemoura

Entrevistador: Adolfo Neto (PPGCA UTFPR) ⁠⁠https://adolfont.github.io/⁠⁠⁠⁠⁠

Nosso site é: ⁠⁠⁠⁠https://fronteirases.github.io/⁠⁠⁠⁠

Opening Song: Extreme Energy (Music Today 80). Composed & Produced by: Anwar Amr Video. Link: ⁠⁠https://www.youtube.com/watch?v=8ZZbAkKNx7s⁠⁠

Links:

• Raciocínio Automatizado com Leonardo de Moura, Pesquisador na Microsoft Research.: https://youtu.be/bwKFcLaeD1A?si=bIXi6CC0V-OZWcEO.

• Tese de Doutorado https://bit.ly/3smu940 

• Vídeos da comunidade Lean https://www.youtube.com/@leanprovercommunity5485/videos 

• (Nature) Mathematicians welcome computer-assisted proof in ‘grand unification’ theory https://www.nature.com/articles/d41586-021-01627-2 

• Histórico do site de Lean https://web.archive.org/web/*/https://leanprover.github.io/ e https://web.archive.org/web/*/http://leanprover.net/

• 16 Linguagens em 16 Dias: Minha Saga da Rinha de Backend https://youtu.be/EifK2a_5K_U?si=xSlY-RFXGvrPah-k   

• “The Economics of Programming Languages” by Evan Czaplicki (Strange Loop 2023) https://www.youtube.com/watch?v=XZ3w_jec1v8 

• Exploring the Lean4 Language https://blog.codeminer42.com/exploring-lean4/ 

• Lean4: Crafting in an Uncharted Territory https://blog.codeminer42.com/overcoming-challenges-and-crafting-in-the-uncharted-territory-of-lean4/ 

• Exploring Lean4, Sofia Rodrigues https://www.youtube.com/watch?v=klooP9cJHCs 

• Morph: The personal AI proof engineer - https://morph.so/blog/the-personal-ai-proof-engineer/ 

• Grupo de Estudos em Haskell da UFABC https://haskell.pesquisa.ufabc.edu.br/

• Tipos Dependentes https://haskell.pesquisa.ufabc.edu.br/desenvolvimento-orientado-a-tipos/07.dependenttypes/

• Elixir em Foco 32: A linguagem de programação Lean, com Algebraic Sofia e Algebraic Gabi https://www.youtube.com/watch?v=LaN6XzyCqao

• Lean Brasil - Grupo de pessoas interessadas na linguagem de programação Lean https://t.me/leanlangbr 

• Site de Lean https://lean-lang.org/ 

• Completion of the Liquid Tensor Experiment https://leanprover-community.github.io/blog/posts/lte-final/ 

• SATurn: SAT Solver-prover in lean 4 https://github.com/siddhartha-gadgil/Saturn 

• Z3 Theorem Prover https://en.wikipedia.org/wiki/Z3_Theorem_Prover

Data de publicação: 14 de novembro de 2023.