3 ms·
> it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any
by pron 9y ago
> it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again.
This can be done with "tainting" types, which are simple intersection types (even Java has them as one of its new pluggable type systems [1]), and doesn't require dependent types.
[1]: https://checkerframework.org/manual/#tainting-checker https://checkerframework.org/manual/#tainting-checker
- catnaroek 9y agoIt's useless if it's optional.
- pron 9y agoSo is F#.
- catnaroek 9y agoAssuming you mean “dependent types in F#” rather than “F#”, after reading the article, I concluded that these are, in fact, not dependent types, but just so-called “smart constructors”. Since “dependent types in F#” don't exist, it doesn't make sense to ask whether they're useful or useless.
- pron 9y agoI meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.
- catnaroek 9y agoYeah, F# is kind of problematic since you aren't forced to use F# to typefully use F# libraries. Things would be a lot better in a language like Standard ML, where you can either use a library correctly (assuming it exposes the right interfaces) or not use it at all. Hooray for abstraction!