Syl quiere llevar los tipos dependientes en tiempo de compilación a la programación de sistemas

Compile-Time Dependent Types

C++, Rust y Zig ya ofrecen computación en tiempo de compilación, pero con restricciones y sin un sistema de tipos formal. Syl propone un sistema de tipos modal con dos ejes, staticity y erasure, que distingue lo que se conoce al compilar de lo que existe en ejecución. Inspirado en la teoría de tipos de dos niveles de András Kovács y en OxCaml, el lenguaje es dependientemente tipado en compilación y simplemente tipado en ejecución.