3 ms·
I don't know what kind of type system you have in mind then. Do you have an example of language where all array types have a way to check, statically, that all
by remram 3y ago
I don't know what kind of type system you have in mind then. Do you have an example of language where all array types have a way to check, statically, that all indexing operations are in bound? How would that even work? A language without dynamically-sized arrays at all, maybe?
- trealira 3y agoI think you can do this with proof assistants, and with the SPARK version of Ada. You can also do it with a dependent type system. I haven't used it, but from what I've read, in the ATS programming language, which is dependently typed, you can guarantee that array index accesses and pointer arithmetic never goes out of bounds, at the cost of having to pass proof variables explicitly to various functions. This poster goes over how to ensure you don't cause buffer overflows in it: https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-b... https://bluishcoder.co.nz/2018/01/10/capturing-program-invariants-in-ats.html https://bluishcoder.co.nz/2018/01/10/capturing-program-invar... It's a bit obscure; this is the only person who's ever blogged about ATS, as far as I can tell.
- tialaramex 3y agoTwo things. Firstly, it is simply not the case that all constraints must be able to be statically enforced for them to constitute part of the type's definition. I'd guess that's a huge part of the confusion here. But, yes, actually all WUFFS indexing is statically checked. It's using inference to conclude the range of the index, so if it won't fit that's a static type mismatch.