4 ms·
As far as I understand, Idris and dependent typing in general are only useable for small systems today - the largest systems successfully proved using dependent
by simiones 5y ago
As far as I understand, Idris and dependent typing in general are only useable for small systems today - the largest systems successfully proved using dependent typing are the SEL4 kernel (which is ~10k lines of C) and the CompCert C compilers (which compiles a subset of the C language, and has only a minimalistic optimizer, if I remeber correctly). And these two have been 5-10 year PhD projects.