3 ms·
Like Liquid Haskell? http://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html http://www.haskellforall.com/2015/12/compile-time-memory
by david_ar 11y ago
Like Liquid Haskell?
http://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html http://www.haskellforall.com/2015/12/compile-time-memory-saf...
- pron 11y agoWell, yes and no. You can prove all the properties liquid types can without actually using liquid types, just by running the algorithms that infer them. Either way (inferring with or without types) the problem of indexing is undecidable, and cannot be verified in the general case (but it can in many common usages).
- catnaroek 11y agoThe point to using types is that they make static analyses more compositional. Types enforce invariants across module boundaries, without requiring the entire program to be checked in a single pass.
- pron 11y agoYes, but they may also lose information in the process... As usual, it's a tradeoff.
- catnaroek 11y agoYep. That was exactly what I had in mind.