3 ms·
I am impressed by the fact that Typed Closure is a lot of things in addition to language design -- library development, editor/tool development, even community
by nmrm2 11y ago
I am impressed by the fact that Typed Closure is a lot of things in addition to language design -- library development, editor/tool development, even community engagement and evangelism.
> Clojure codebases typically rely on tests to verify the correctness of the code.
OT, but this is a pet peeve of mine. Tests aren't verification, and they cannot demonstrate correctness (without being exhaustive). Clojure codebases typically rely on tests to mitigate the risk of runtime errors.
- JadeNB 11y ago> Tests aren't verification, and they cannot demonstrate correctness (without being exhaustive). Agreed, but it's important to note that there's very little that can demonstrate correctness. Most type systems by themselves don't; as Pierce describes it in TAPL, "[a] type system is a syntactic method for automatically checking the absence of certain erroneous behaviors" (emphasis mine). It's possible that, in a dependent type system, those certain behaviours will be sufficiently many that you can prove the correctness of a program specification, but even a rich system like Haskell's usually doesn't offer such guarantees (just consider `tail []`; or, for an example that's not just a Prelude wart, `take n xs`).
- nmrm2 11y agoIt's difficult to demonstrate full functional correctness. However, it is pretty easy to demonstrate partial correctness. Most tests -- even if they were completely exhaustive -- correspond to partial correctness rather than functional correctness.