Formality é uma linguagem de programação funcional em desenvolvimento, e que será lançada oficialmente ainda esse ano. Ela é uma linguagem bem "hardcore", com tipos dependentes e provas formais, inspirada em Haskell/Agda/Coq, mas com uma série de diferenciais, principalmente no que diz respeito ao runtime (optimal reductions, paralelismo, runtime fusion, etc.), visando combinar todo esse alto nível matemático com o potencial de ser realmente eficiente na prática. Essa é a carinha atual dela:
// Datatypes estilo Haskell
// O tipo de números naturais
T Nat
| succ {pred : Nat}
| zero
// Uma função simples
pred : {|n : Nat} -> Nat
| succ = n.pred
| zero = zero
// Uma função "recursiva"
double :! {|*n : Nat} -> Nat
| succ = succ(succ(double(n.pred)))
| zero = zero
// Datatypes estilo Agda
// Um vetor de elementos cujo tamanho é conhecido estaticamente
T Vector <A : Type> {len : Nat}
| vpush {~len : Nat, head : A, tail : Vector(A, len)} & succ(len)
| vempty & zero
// Uma função head que é estaticamentet impossível de ser chamada em um vetor vazio
vhead : {~T : Type, n : Nat, vector : Vector(T, succ(n))} -> T
case<Vector> vector
| vpush => head
| vempty => 0
: case<Nat> len
| succ => T
| zero => U32
: Type
// Provas estilo Agda
// Igualdade proposicional (um tipo que diz, estaticamente, que "a == b")
T Eq <A : Type> {a : A, b : A}
| refl {~a : A} : Eq(A, a, a)
// Simetria da igualdade (uma prova que "a == b" implica "b == a")
sym : {~A : Type, ~a : A, ~b : A, e : Eq(A, a, b)} -> Eq(A, b, a)
case<Eq> e
| refl => refl<A>(~a)
: Eq(A, b, a)Punk né? Se nada disso aí faz sentido, não se assuste nem fuja. Acredite, isso aí já é MUITO mais simples do que as versões iniciais onde tudo era codificado com lambdas, principalmente pois estamos nos aproximando da usabilidade do Agda e do Haskell. Mas vai melhorar ainda mais, e nosso maior sonho é torná-la um dia quase tão amigável quanto linguagens mais simples como Python e JavaScript.
O Formality começou com o apoio da Fundação Ethereum. Agora, com apoio da Fundação Ethereum e de outras plataformas de crypto, estamos criando nossa própria empresa, a Sunshine Cybernetics, voltada a desenvolvê-lo. Atualmente contamos com cerca de 10 devs.
O tempo e experiência me fizeram concluir que tipos são desejáveis. Por isso, Formality é muito similar ao Agda, Coq, Haskell. Isso significa que o sistema de tipos é tão expressivo que se torna capaz de codificar teoremas matemáticos. Isso é, ao invés de "essa função recebe um int e retorna uma lista de ints", podemos dizer algo como "essa função recebe um int N, e retorna uma lista xs de inteiros primos tal que mul(xs) == N". Consegue perceber que função é essa? O fato de que um sistema de tipos suficientemente forte é a ponte para ligar os campos da programação e da matemática é particularmente incrível!
O maior diferencial do Formality com relação ao Agda, ao Coq, e até do Haskell, é que ele é executado de forma ótima. Isso é, ele é "asintóticamente" mais rápido que todas as outras linguagens na tarefa de "computar lambdas", o que pode ser explorado em vários casos, e tem diversas implicações que o tornam único.
Sabe quando você usa um monte de maps, filters, reduces em sequência, e fica imaginando o custo que todas essas alocações temporárias vai ter? Linguagens como Haskell são capazes de eliminar todas essas estruturas intermediárias através de algoritmos de fusão (deforesting, foldr/build, stream fusion, etc.), e esse é um dos motivos que o torna tão rápido mesmo sendo tão alto nível. O problema é que essas otimizações são "hardcoded" no compilador do Haskell, só funcionam com código estático. O Formality é capaz de aplicar essas otimizações durante o runtime. Ou seja, ele é capaz não só de eliminar estruturas as intermediárias dos maps e filters da vida, mas também de otimizar e aperfeiçoar seu programa conforme ele é executado, levando em conta seus inputs de runtime.
Assim como Rust, C e C++, o Formality não precisa de um garbage collector global, a memória é liberada imediatamente, assim que um valor sai de escopo. Apesar disso, esse fato quase não é sentido na usabilidade da linguagem, e ela mantém um estilo alto nível similar ao Haskell e ao Agda.
A linguagem como um todo é massivamente paralela, o que significa que cada operação, por menor que seja, pode ser executada em paralelo, através de um sistema de reduções confluentes em grafos chamado "interaction combinators".
Diferentemente do que dizem por aí, ser Turing-completo não é difícil. Pelo contrário, hoje em dia você espirra e sai uma linguagem Turing-completa. Difícil é ser Turing-incompleto, ou seja, incapaz de emular uma máquina de Turing, e, ao mesmo tempo, expressivo e poderoso o suficiente para expressar qualquer programa que se queira escrever na prática. Ser Turing-incompleto traz uma série de vantagens; por exemplo, seus programas jamais poderão entrar em um loop infinito, malandramente "resolvendo" o problema da parada. Também é importante para a consistência. Existem diversas maneiras de evitar que uma linguagem se torne Turing-completa. Por exemplo, o Agda permite apenas recursão estrutural. Outras linguagens colocam um bound explícito na quantidade de loops ou recursões que você pode fazer. Mas essas soluções são, na minha opinião, meio "hardcoded", para não dizer "gambiarradas". O Formality é Turing-incompleto por um motivo, ao meu ver, bonito e elegante: ele opera através de uma lógica diferente da lógica clássica ou da lógica intuitionista: a lógica elementar afina, que, graças ao seu sistema de camadas, é "naturalmente terminante". Você pode ler mais sobre isso aqui.
Eu pessoalmente aredito que optimal reductions possam levar a novas descobertas no campo da teoria de complexidade. Por exemplo, um algoritmo de fatoração em tempo polinomial no Formality não me surpreenderia. Interessantemente, o Formality demonstra uma performance assustadora na função de modularização exponencial, que é uma das chaves do algoritmo de Shor. É claro, isso é só uma intuição, mas vai que? Escrevi mais sobre isso aqui: https://gist.github.com/MaiaVictor/e556062185c5863d814980123e03630f
O core da linguagem, incluindo interpretador e o sistema de tipos, cabe por inteiro em 1000 linhas de código. Eu julgo isso importante, porque eu acredito que todo algoritmo / prova matemática deve ser reduzido para um pequeno conjunto de axiomas que seja facilmente verificável. O problema é que é MUITO difícil ter um sistema de tipos indutivos consistente que não precise de milhares de linhas de código pra ser implementado, mas, a mesma característica que o torna compatível com optimal reductions também o permite codificar tipos indutivos através de "self-encodinigs" (algo bem simples de implementar) de forma consistente, o que acabou sendo uma coincidência extremamente feliz. Você pode ler mais sobre isso aqui.
NÃO! Existe uma diferença enorme entre velocidade assintótica (teórica) e prática. Tudo isso acima é verdade: em muitos programas, o Formality destrói Haskell, C, Rust e qualquer outra linguagem do mundo, por conta de ser assintóticamente eficiente. O Formality é, sim, mais rápido em teoria. Mas o GHC teve décadas de otimizações pra chegar onde está. Por isso, na prática, programas de Formality mais "simples" que não exploram optimal reductions, paralelismo, etc., vão ser bem mais lerdos que os de Haskell, por conta do overhead do seu runtime. Eu acredito que isso seja algo temporáriio, e que seja uma questão de tempo e engenharia para que o Formality se torne mais rápido até no pior caso.
Como eu disse, estamos em uma fase pré release oficial, tudo ainda é muito novo. Para começar a usar o Formality, você precisa instalá-lo com o npm i -g formality-lang. O problema é que ainda não temos documentação dele, apenas do seu core não tipado, nesse link aqui, mas a sintaxe não é a mesma. Se você realmente quiser, pode dar uma olhada nesse arquivo daqui, onde eu escrevi os primeiros programas do Formality. Mas não recomendo fazer isso. Por hora, o melhor que você pode fazer é só entrar no grupo, seguir nossos repositórios, fazer perguntas e acompanhar o desenvolvimento. Provavelmente até o final da semana que vem já teremos uma documentação inicial e libs pro Formality!