Um interessante trabalho com este nome foi pré-publicado no site ArXiv no dia 4 de março último [dia em que o blog nasceu], apresentando a linguagem de programação Catala. Segundo seus criadores “é uma linguagem adaptada para programação sócio-fiscal-legislativa; uma linguagem que imita a estrutura lógica da lei”. A estrutura lógica da linguagem foi formalizada pela Professora Sarah Lawsky em seu artigo “Uma Lógica para Estatutos”. Apresentamos o resumo do artigo do ArXiv e os comentários do blog a respeito.

Catala: A Programming Language for the Law
DENIS MERIGOUX, Inria, France
NICOLAS CHATAING, Inria ENS Paris, France
JONATHAN PROTZENKO, Microsoft Research, USA

Resumo

A lei em geral sustenta a sociedade moderna, codificando e governando muitos aspectos da vida diária dos cidadãos. Muitas vezes, a lei está sujeita a interpretação, debate e contestação em vários tribunais e jurisdições. Mas em algumas outras áreas, o direito deixa pouco espaço para interpretação e visa essencialmente descrever com rigor um cálculo, um procedimento de decisão ou, simplesmente, um algoritmo. Infelizmente, a prosa sempre foi uma ferramenta lamentavelmente inadequada para o trabalho. A falta de formalismo deixa espaço para ambiguidades; a estrutura dos estatutos legais, com muitos parágrafos e subseções espalhados por várias páginas, torna difícil calcular o resultado pretendido do algoritmo subjacente a um determinado texto; e, como acontece com um software crítico mal especificado, o uso de linguagem informal deixa os casos mais difíceis sem solução.

Apresentamos Catala, uma nova linguagem de programação que projetamos especificamente para permitir uma tradução direta e sistemática da lei estatutária em uma implementação executável. Catala tem como objetivo reunir advogados e programadores através de um meio compartilhado, onde juntos eles possam entender, editar e evoluir, preenchendo uma lacuna que muitas vezes resulta em implementações dramaticamente incorretas da lei.

Implementamos um compilador para Catala e provamos a exatidão de suas etapas principais de compilação usando o assistente de prova F *. Avaliamos Catala em vários textos legais – que são algoritmos disfarçados, notadamente a seção 121 do imposto de renda federal dos Estados Unidos e os benefícios familiares bizantinos da França; ao fazer isso, descobrimos um “bug” na implementação oficial da lei . Observamos, como consequência do processo de formalização da linguagem, que o uso da Catala permite ricas interações entre advogados e programadores, levando a uma maior compreensão da intenção legislativa original, enquanto produz uma especificação executável “correta-por-construção”, reutilizável por um ecossistema de software maior.

Link para o trabalho na íntegra

Minhas considerações

Voltando aqui para o home office, eu diria, em minha modesta opinião, que o fato de uma lei ser internamente consistente e livre de lacunas não significa necessariamente que ela seja uma boa lei. Uma abordagem algorítmica para a criação de tais procedimentos corre o risco de se tornar muito cientificista e automática [daí autoritária], de modo que podemos acabar com um grande corpo de leis que não pode ser questionado “porque foi ‘provado’ que está correto”. Lembro-me de uma observação que [o cientista da computação e matemático] Donald Knuth fez a respeito de um certo trecho de código. Era mais ou menos assim: “Cuidado ao usar isto; eu apenas provei que está correto, mas não tentei executá-lo”.

Por outro lado, o resumo do trabalho menciona que eles já descobriram um “bug” em uma lei ativa ao reescrevê-la em sua linguagem computacional. Portanto, essa pode ser uma ferramenta extremamente útil para encontrar casos extremos e brechas na legislação. E novamente, como o resumo menciona, para minha tranquilidade, o projeto se destina a leis que devem ser interpretadas 100% literalmente como um algoritmo. Essas leis existem e são exatamente aquelas que deveriam ser absolutamente consistentes.

Vou dar um exemplo de um campo em que, imagino, a lei e os contratos devem ser interpretados 100% literalmente como um algoritmo: finanças estruturadas. O prospecto de um título estruturado, por exemplo um título hipotecário, consiste normalmente de cem ou mais páginas de um texto jurídico muito denso, que foi trabalhado intensamente por advogados e banqueiros altamente especializados durante meses. Sua intenção é criar, digamos, uma empresa, de propósito específico, com regras rígidas sobre como operar até o último centavo, e discrição zero. Isso permite que os investidores (em teoria) entendam como será o desempenho do título.

Na literatura introdutória à análise de crédito estruturado, que tenho estudado, um dos autores diz que nunca leu um prospecto para um título estruturado que não contivesse erros de redação. Esse é um tipo de erro que não pode ser encontrado por um sistema formal determinístico, como a máquina de Turing de nossos computadores.

Eu concordo com o sentimento, no que se refere aos erros. De fato, os engenheiros têm a capacidade de automatizar alguns problemas muito complexos, mas sempre haverá uma classe de problemas além da automação, simulação, análise, etc. Temos apenas que aceitar que a única maneira de resolvê-los é com trabalho lento, difícil e sujeito a erros. Algumas coisas são simplesmente complexas demais para se fazer [note que estamos falando de computação clássica].

Essa é uma novidade sofisticada da qual se espera que ajude a evitar erros, reduzir custos do sistema jurídico, aumentar a consistência, etc. Tenho a impressão, porém, que ela será aplicada às leis existentes de forma mais geral do que o resumo parece sugerir.

Novas leis serão feitas com esse novo fator em mente, aumentando a aplicação da ideia, independentemente de as novas leis serem ou não interpretáveis ​​literalmente. Catala provavelmente não causará uma revolução jurídica amanhã, mas espero que possa ser o início de uma lenta reforma em direção à precisão linguística e à compatibilidade com as máquinas na legislação do futuro.

Post Scriptum

Um texto sobre linguagem de programação não poderia estar completo sem um exemplo da sintaxe. Pensei em dar uma mostra interessante e bastante genérica de como a Catala poderia ser implementada. Isso motivou uma visita ao wiki para pesquisar algum exemplo histórico de dispositivo legal. O que descobri não podia ser mais a propósito: o código de Ur-Nammu [ver DuckDulckGo ou Google], a mais antiga peça de legislação que se conhece. Escolhi como exemplo o artigo 14, que me parece bem em linha com os mores de nosso tempo, e que dispõe basicamente:

Se um homem acusou a esposa de um homem de adultério, e a provação do rio provar sua inocência, então o homem que a acusou deve pagar um terço de uma mina de prata.

Código de Ur-Nammu, art. 14

Eis a justiça em ação. Se ela se afogar, ela é culpada. Se ela sobreviver, alguém receberá 1/3 de uma mina de prata. O rei Ur-Nammu é vago aqui quanto a quem fica com o dinheiro. Provavelmente o marido.

Como poderíamos codificar isso em Catala? Vou começar, e quem quiser pode contribuir nos comentários:

declaration structure Pessoa:
    data id content integer

  declaration structure Periodo:
    data inicio content date
    data fim content date

  declaration structure CasalCasado:
    data adulterio_data content date
    data marido content Pessoa
    data mulher content Pessoa
   
  declaration structure AcusacaoDeAdulterio:
    data casal1 content CasalCasado
    data acusador content Pessoa
    data adulterio_data content Periodo
   
  declaration structure Rio
    data id content integer
 
  declaration structure ProvacaoPelaAgua:
    data acusado content Pessoa
    data rio1 content Rio
    data data_da_provacao content Periodo

  declaration scope LeiDeUrNammu:
    context requisitos_atendem condicao
    context casados_atendem condicao
    context acusado_enquanto_casado_atende condicao
    context provado_pela_água_atende condicao

Conceito da Linguagem (Segundo os criadores, no GitHub)

Catala é uma linguagem adaptada para a programação sócio-fiscal ancorada na legislação. Ao anotar cada linha do texto legislativo com seu significado em termos de código, pode-se derivar uma implementação dos complexos mecanismos sócio-fiscais que apresentam um alto nível de segurança quanto à fidelidade do código-lei.

Concretamente, primeiro você deve reunir todas as leis, ordens executivas, casos anteriores, etc. que contenham informações sobre o mecanismo sócio-fiscal que você deseja implementar. Em seguida, você pode prosseguir para anotar o texto artigo por artigo, em seu editor de texto favorito:

Depois que seu código estiver completo e testado, você pode usar o compilador Catala para produzir uma versão PDF de sua implementação legível por advogado. A linguagem Catala foi especialmente desenvolvida em colaboração com profissionais do direito para garantir que o código possa ser revisado e certificado como correto pelos especialistas de domínio, que neste caso são advogados e não programadores.