4 ms·

At what point would you stop with formal static verification and why would you stop? At which point would you concede you’ve gone too far, and why? Do you have

At what point would you stop with formal static verification and why would you stop? At which point would you concede you’ve gone too far, and why? Do you have a criteria? Or are you convinced that as much formal verification as possible is the biggest win? How are you sure you are solving the developer throughout problem optimally by using machine proof methods? Any static type enthusiast should have a clear and unminced answer to these questions. Or I smell snake oil.

whateveracct 7y ago
I'd say I have as much of a criteria as programmers in other language have regarding their code style and organization. Coding in the small is about a lot of judgment calls, and Haskell is the same. The only argument I've heard is you can't trust people to write good Haskell because they have too many options. But I have more respect for my fellow professionals than that :) If it feels like it'll save me from making errors and it's easy to implement, I tend to use it. Or if encoding something in types ends up allowing for greater introspection and automation. For instance, if I want my FFI bindings to allow the user to allocate some buffers up-front and reuse them for added performance, I may use the ST trick and CPS to ensure that that manually-allocated memory is used properly (e.g. not used after being freed.) That's a great example because it isn't a very hard bit of library code to implement or use, but it uses Haskell's fancy types to do it. Another example of this is using Void to type infinite loops (e.g. IO Void). Then when I handle exceptions either synchronously or from a thread, I can replace a comment of "should never happen" in the no-exception case with a call to `absurd`. Once again, doing this has little-to-no added cost, but the benefits are real (and get realer in less trivial examples)..and languages like Python and Go and Java just can't do them. Feels strictly better to me. The Haskell type system is just a set of tools I can use to organize my software and help ensure it's both ergonomic and easy to use. Other languages have tools for these tasks as well. It's just that Haskell's let you configure static analysis in-the-language itself.
- wellpast 7y ago
  > The Haskell type system is just a set of tools I can use to organize my software and help ensure it's both ergonomic and easy to use. If it were “just a set of tools” then it would be weakly typed. Tools are by their very nature a la carte and don’t insist upon themselves. Strong static typing insists itself; otherwise it’d be a la carte/optional/weak. Edit: typo
  - whateveracct 7y ago
    I can choose how typed my code is. The existence of extremely strong typing facilities doesn't mean I have to use them to the max at every turn. Hence, the types are a set of tools I can use to craft interfaces. And the fact that I can impose constraints on my callers so that they can't accidentally call my code wrong, all the better. And in my experience, despite Haskell being quite niche, its library quality and ease-of-use is very good. The ecosystem's main weakness is lack of libraries for things period. When they exist, they tend to be nice. Types help with this directly as well.
    - wellpast 7y ago
      > I can impose constraints on my callers so that they can't accidentally call my code wrong, all the better. This is precisely the mentality that impedes productivity in typical business delivery case. If your callers are not thinking in terms of contracts (precondition/postcondition) then you've hired the wrong "callers"; some amount of type checking may save you in some cases but your function contracts go far, far beyond the type signature - and here, with callers you can't trust, you're screwed anyway and types won't save you (and it sounds like they've given you a false sense of security.) Better to build a process and expertise that increases correctness for the entire function contract not just the narrow bit that can be expressed in a type.
      - whateveracct 7y ago
        Haskell function contracts don't tend to go that far beyond a type signature. Partially because what can be expressed in the type isn't that narrow nowadays. The situation you're describing is a gigantic strawman per my years of professional FP experience.

whateveracct 7y ago

I'd say I have as much of a criteria as programmers in other language have regarding their code style and organization. Coding in the small is about a lot of judgment calls, and Haskell is the same. The only argument I've heard is you can't trust people to write good Haskell because they have too many options. But I have more respect for my fellow professionals than that :) If it feels like it'll save me from making errors and it's easy to implement, I tend to use it. Or if encoding something in types ends up allowing for greater introspection and automation. For instance, if I want my FFI bindings to allow the user to allocate some buffers up-front and reuse them for added performance, I may use the ST trick and CPS to ensure that that manually-allocated memory is used properly (e.g. not used after being freed.) That's a great example because it isn't a very hard bit of library code to implement or use, but it uses Haskell's fancy types to do it. Another example of this is using Void to type infinite loops (e.g. IO Void). Then when I handle exceptions either synchronously or from a thread, I can replace a comment of "should never happen" in the no-exception case with a call to `absurd`. Once again, doing this has little-to-no added cost, but the benefits are real (and get realer in less trivial examples)..and languages like Python and Go and Java just can't do them. Feels strictly better to me. The Haskell type system is just a set of tools I can use to organize my software and help ensure it's both ergonomic and easy to use. Other languages have tools for these tasks as well. It's just that Haskell's let you configure static analysis in-the-language itself.

wellpast 7y ago
> The Haskell type system is just a set of tools I can use to organize my software and help ensure it's both ergonomic and easy to use. If it were “just a set of tools” then it would be weakly typed. Tools are by their very nature a la carte and don’t insist upon themselves. Strong static typing insists itself; otherwise it’d be a la carte/optional/weak. Edit: typo
- whateveracct 7y ago
  I can choose how typed my code is. The existence of extremely strong typing facilities doesn't mean I have to use them to the max at every turn. Hence, the types are a set of tools I can use to craft interfaces. And the fact that I can impose constraints on my callers so that they can't accidentally call my code wrong, all the better. And in my experience, despite Haskell being quite niche, its library quality and ease-of-use is very good. The ecosystem's main weakness is lack of libraries for things period. When they exist, they tend to be nice. Types help with this directly as well.
  - wellpast 7y ago
    > I can impose constraints on my callers so that they can't accidentally call my code wrong, all the better. This is precisely the mentality that impedes productivity in typical business delivery case. If your callers are not thinking in terms of contracts (precondition/postcondition) then you've hired the wrong "callers"; some amount of type checking may save you in some cases but your function contracts go far, far beyond the type signature - and here, with callers you can't trust, you're screwed anyway and types won't save you (and it sounds like they've given you a false sense of security.) Better to build a process and expertise that increases correctness for the entire function contract not just the narrow bit that can be expressed in a type.
    - whateveracct 7y ago
      Haskell function contracts don't tend to go that far beyond a type signature. Partially because what can be expressed in the type isn't that narrow nowadays. The situation you're describing is a gigantic strawman per my years of professional FP experience.