4 ms·

Yes, that's the whole point of static analysis, to move runtime checks to compile time Move simple runtime checks to compile time. Most if not all of these can

Yes, that's the whole point of static analysis, to move runtime checks to compile time Move simple runtime checks to compile time. Most if not all of these can be done with iterators or simple loops. Index lookups that depend on use input and data still have to be checked somewhere and should probably be done outside of a loop anyway. Static analysis is always welcome, but this seems like a lot to go through to solve something that isn't much of an issue in the first place. Bounds checks were a big problem in C, but with more explicit iteration and runtime checks they are almost never a problem I see anymore.

one-punch 3y ago
> this seems like a lot to go through to solve something that isn't much of an issue in the first place...but with more explicit iteration and runtime checks they are almost never a problem I see anymore. If you can afford runtime checks (if they are not much of an issue in the first place), Haskell, C++, Rust, and Julia can have runtime checks. If you want to opt-out of runtime checks, Haskell, C++, Rust, and Julia can opt-out easily, but unsafely. So, to be fair to Haskell or any of them, this is not a complication specific only to Haskell. But Haskell enables you to do more. With around 30 lines of Liquid Haskell (those lines between {-@ and @-}), you can upgrade simple runtime checks to compile time verification, see the full example [1]. You get great efficiency, safely, without unnecessary runtime checks, which is impossible in C++, Rust, or Julia without Liquid Types. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md#full-program https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell"
- CyberDildonics 3y ago
  you can upgrade simple runtime checks to compile time verification These aren't the same though. Runtime checks can check every access, static analysis isn't going to deal with every scenario like access based on inputs. Lumping them together is pretending there is something happening that isn't.
  - one-punch 3y ago
    > static analysis isn't going to deal with every scenario like access based on inputs. Not true. With proper abstraction, static analysis proves the absence of bugs under all relevant inputs, which gives stronger guarantees than testing at development time (which only checks for a number of inputs), and is more performant than runtime checks (without runtime overhead). An example is the use of a static type system, which eliminates a whole class of bugs under all possible values of the same type (those due to type mismatch: passing a string into a function expecting an integer), which is stronger than a test suite testing certain inputs, and does not have runtime overhead (unlike runtime checks). Going further than usual type systems, people study refining types by possible values (such as positive integers as a refinement of all integers), and the result is refinement types, which is what Liquid Types is based on. And you can see this in action in the full example [1], such as { n : Int | 0 <= n } which refines n to be a positive integer. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell" > Lumping them together is pretending there is something happening that isn't. Correct. Static analysis can formally verify correctness under every access (like runtime checks), but without the runtime overhead (unlike runtime checks), with proper abstraction. That is why compile time verification is an upgrade from runtime checks. OK, in reality the trick is that static analysis removes redundant runtime checks (check exactly once), see the sibling discussion https://news.ycombinator.com/item?id=37376963 https://news.ycombinator.com/item?id=37376963. PS: I figured that setting the record strict may benefit others, such as https://news.ycombinator.com/item?id=37380176 https://news.ycombinator.com/item?id=37380176, hence this reply.
    - CyberDildonics 3y ago
      static analysis removes redundant runtime checks Seems like back peddling. If part of the input data you have is there to reference input data in an array in C++ you would check the input data ahead of time so that you don't have to check the range in the middle of a loop. Then you can have performance that is compared to everything else instead of just other programs written in the same language.
- eigenspace 3y ago
  > But Haskell enables you to do more. With around 30 lines of Liquid Haskell (those lines between {-@ and @-}), you can upgrade simple runtime checks to compile time verification, see the full example [1]. You get great efficiency, safely, without unnecessary runtime checks, which is impossible in C++, Rust, or Julia without Liquid Types. Just a side-note, julia's compiler is very adept at proving situations where array accesses are guaranteed to be in-bounds and will automatically elide bounds checks in those situations. Not saying this to take anything away from Liquid Haskell though, that seems like a very cool project with some very cool capabilities.
  - one-punch 3y ago
    Thanks for the great note, I learned something today.

one-punch 3y ago

> this seems like a lot to go through to solve something that isn't much of an issue in the first place...but with more explicit iteration and runtime checks they are almost never a problem I see anymore. If you can afford runtime checks (if they are not much of an issue in the first place), Haskell, C++, Rust, and Julia can have runtime checks. If you want to opt-out of runtime checks, Haskell, C++, Rust, and Julia can opt-out easily, but unsafely. So, to be fair to Haskell or any of them, this is not a complication specific only to Haskell. But Haskell enables you to do more. With around 30 lines of Liquid Haskell (those lines between {-@ and @-}), you can upgrade simple runtime checks to compile time verification, see the full example [1]. You get great efficiency, safely, without unnecessary runtime checks, which is impossible in C++, Rust, or Julia without Liquid Types. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md#full-program https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell"

CyberDildonics 3y ago
you can upgrade simple runtime checks to compile time verification These aren't the same though. Runtime checks can check every access, static analysis isn't going to deal with every scenario like access based on inputs. Lumping them together is pretending there is something happening that isn't.
- one-punch 3y ago
  > static analysis isn't going to deal with every scenario like access based on inputs. Not true. With proper abstraction, static analysis proves the absence of bugs under all relevant inputs, which gives stronger guarantees than testing at development time (which only checks for a number of inputs), and is more performant than runtime checks (without runtime overhead). An example is the use of a static type system, which eliminates a whole class of bugs under all possible values of the same type (those due to type mismatch: passing a string into a function expecting an integer), which is stronger than a test suite testing certain inputs, and does not have runtime overhead (unlike runtime checks). Going further than usual type systems, people study refining types by possible values (such as positive integers as a refinement of all integers), and the result is refinement types, which is what Liquid Types is based on. And you can see this in action in the full example [1], such as { n : Int | 0 <= n } which refines n to be a positive integer. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell" > Lumping them together is pretending there is something happening that isn't. Correct. Static analysis can formally verify correctness under every access (like runtime checks), but without the runtime overhead (unlike runtime checks), with proper abstraction. That is why compile time verification is an upgrade from runtime checks. OK, in reality the trick is that static analysis removes redundant runtime checks (check exactly once), see the sibling discussion https://news.ycombinator.com/item?id=37376963 https://news.ycombinator.com/item?id=37376963. PS: I figured that setting the record strict may benefit others, such as https://news.ycombinator.com/item?id=37380176 https://news.ycombinator.com/item?id=37380176, hence this reply.
  - CyberDildonics 3y ago
    static analysis removes redundant runtime checks Seems like back peddling. If part of the input data you have is there to reference input data in an array in C++ you would check the input data ahead of time so that you don't have to check the range in the middle of a loop. Then you can have performance that is compared to everything else instead of just other programs written in the same language.
eigenspace 3y ago
> But Haskell enables you to do more. With around 30 lines of Liquid Haskell (those lines between {-@ and @-}), you can upgrade simple runtime checks to compile time verification, see the full example [1]. You get great efficiency, safely, without unnecessary runtime checks, which is impossible in C++, Rust, or Julia without Liquid Types. Just a side-note, julia's compiler is very adept at proving situations where array accesses are guaranteed to be in-bounds and will automatically elide bounds checks in those situations. Not saying this to take anything away from Liquid Haskell though, that seems like a very cool project with some very cool capabilities.
- one-punch 3y ago
  Thanks for the great note, I learned something today.