Type Checking in Rust per il kernel di Lean 4

Questa tesi si propone di sviluppare un type checker in Rust per l'export del linguaggio Lean. L'obiettivo principale è quello di realizzare un sistema indipendente in grado di verificare la correttezza delle dimostrazioni prodotte da Lean. Infatti, poiché il kernel di Lean è responsabile della validazione logica delle prove, un eventuale bug al suo interno potrebbe compromettere l'affidabilità dei risultati. Reimplementando il kernel in modo autonomo si riduce il rischio di replicare gli stessi errori, aumentando così la probabilità di individuare eventuali incongruenze o bug nascosti nelle dimostrazioni. Inoltre, disporre di una versione indipendente del kernel consente una maggiore libertà di intervento sulle strutture dati e sugli algoritmi, facilitando l'esplorazione di possibili ottimizzazioni e miglioramenti prestazionali. Il programma, come primo passo, deve leggere il file di export e memorizzare tutte le informazioni in esso contenute, suddividendole in base alla loro tipologia e verificando che ciascuna informazione sia valida. Successivamente, deve controllare che le dimostrazioni siano state definite correttamente, verificando i tipi delle dimostrazioni e, qualora presenti, che i valori al loro interno siano di tipo compatibile.