Vide https://condadobraveheart.com/threads/desafio-codigo-maldito.7958/
A linguagem escolhida foi Lean 4.
Para tornar o código o mais maldito possível, os três paradigmas foram implementados na mesma linguagem. Os programas estão em arquivos distintos:
MainFunc.lean: Implementação puramente funcional. Na prática, como Lean é uma linguagem puramente funcional, todas as implementações são puramente funcionais. Essa, em particular, evita usar syntax sugar relacionado a estruturas de repetição, e segue uma implementação mais padrão de linguagens funcionais, que também permite uma prova de correção mais simples (vide teoremarun_passAround_respects_likesno arquivo).MainStructured.lean: Implementação estruturada. Essa implementação é estruturada no sentido de Edsger W. Dijkstra e do teorema de Böhm–Jacopini: o programa é composto estritamente por comandos sequenciais, condicionais, e blocos de repetição.MainOOP.lean: Implementação orientada a objetos. A orientação a objetos é implementada através de passagem de mensagens, e objetos são opacos (i.e. encapsulamento é garantido por construção).
Todas as implementações usam como base as definições básicas dos tipos usados para as crianças e os brinquedos, e a função de gostos de cada criança.
Essas definições, bem como os teoremas que provam que a função de gostos definida corresponde à
única função possível obedecendo os axiomas dados no enunciado do desafio, estão no arquivo
Cursed/Basic.lean.
O projeto usa Lake como sistema de construção.
A forma mais fácil de obter uma instalação funcional do Lake é através do gerenciador de versão do Lean (elan).
Feito isso, basta executar cada programa com o comando correspondente do Lake:
lake exe cursed-func
lake exe cursed-structured
lake exe cursed-oopObs.: A compilação depende da biblioteca de matemática do Lean (Mathlib), e portanto a primeira compilação pode ser relativamente custosa.