4 ms·
Dependent types is what you're searching for. Mostly used by (functional) proof 'languages' like Coq, Agda, Idris. For a language to have dependent types, the v
by ReleaseCandidat 5y ago
Dependent types is what you're searching for.
Mostly used by (functional) proof 'languages' like Coq, Agda, Idris. For a language to have dependent types, the values that the types depend on must not (like with Rust) only be compile time constants, but values at runtime.
- tialaramex 5y agoHuh, surely the types in WUFFS are offering what the parent wanted (WUFFS won't let you add two 32-bit signed integers x and y together unless you've explicitly constrained them so that this operation won't overflow or underflow) but purely enforced at compile time since WUFFS wants to go real fast? WUFFS is in a related place to something like Coq. The idea in WUFFS is, if I write my decoder for the FOO image format in WUFFS, no matter how lazy and incompetent I am, your image displaying program can confidently use my FOO decoder, and if I did a bad enough job it might be slow or produce the wrong picture but it can't crash or run a SSH server or delete the password database or whatever.