7 ms·

> 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 o

> 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.
- one-punch 3y ago
  I think the main confusion is that, "Scrap your Bounds Checks with Liquid Haskell" presented a toy example/implementation which scales to real implementations, for the task of high-performance parsing of UDP packets (used by Awake Security, I guess). The toy example/implementation is chosen to teach Liquid Types/Haskell, and therefore, covers the simple case of parsing UDP headers, which is a simple bounds check of "indexing an array of length 8". In this case, there is no need to use Liquid Types in any language. But in the real use case (not shown in the talk), when you want to dig deeper into the content of UDP packets and such, you will need more than "check the input data (length) ahead of time so that you don't have to check the range in the middle of a loop". This is the case where Liquid Types help, tremendously. But such complicated cases, where Liquid Types shines, may not fit into a talk. Again, it is not fair to think this is a complication specific to Haskell.
  - CyberDildonics 3y ago
    Again, it is not fair to think this is a complication specific to Haskell. It is fair, because other languages have a single keyword or setting instead of a whole 'type system' with fancy labels that introduces lots of complexity for something simple.
    - one-punch 3y ago
      It is not fair to think this is a complication specific to Haskell, because you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia, with functions such as unsafeTake and unsafeDrop. https://news.ycombinator.com/item?id=37382215 https://news.ycombinator.com/item?id=37382215 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. https://news.ycombinator.com/item?id=37387005 https://news.ycombinator.com/item?id=37387005 It is unfair to not respond to these points, while calling "this is a complication specific to Haskell." Because Haskell can do what others can do, but more. > lots of complexity for something simple. "indexing an array of length 8" for parsing UDP headers is simple, agreed. And Haskell can handle that simply with unsafe functions. Keeping track of properties with complicated dependencies to parse arbitrary content (perhaps application-logic-aware contents, not "just checking for array length before indexing in a loop") is simple, strong disagree. See the section "Beyond Bounds Checking" of "Why Liquid Haskell matters" for example [1]. This might be used to implement the kinds of static analysis needed for Mojo or Swift, for instance [2]. [1]: https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ "Why Liquid Haskell matters" [2]: https://github.com/modularml/mojo/discussions/466 https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism" https://news.ycombinator.com/item?id=37376010 https://news.ycombinator.com/item?id=37376010 And this cannot be solved in the languages you mentioned, either. Unless you are claiming that all parsing checks are "just checking for array length before indexing in a loop". https://news.ycombinator.com/item?id=37416911 https://news.ycombinator.com/item?id=37416911 We are still working on completely different scales. The talk is using a toy example to show what is possible, and you are using that example too literally, without realizing that the example scales to handle much more complex problems that people need to deal with in the real world. It is unfair to lump together different scales and call them the same thing. Your reaction is like criticizing a talk which shows sorting 5 numbers with programs, with "it is simple to sort 5 numbers by hand, why bother learning how to program with all those complexity for something this simple?". And then calling this fair, without realizing that in the real world, sometimes people need to sort way more than 5 numbers.

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.

one-punch 3y ago
I think the main confusion is that, "Scrap your Bounds Checks with Liquid Haskell" presented a toy example/implementation which scales to real implementations, for the task of high-performance parsing of UDP packets (used by Awake Security, I guess). The toy example/implementation is chosen to teach Liquid Types/Haskell, and therefore, covers the simple case of parsing UDP headers, which is a simple bounds check of "indexing an array of length 8". In this case, there is no need to use Liquid Types in any language. But in the real use case (not shown in the talk), when you want to dig deeper into the content of UDP packets and such, you will need more than "check the input data (length) ahead of time so that you don't have to check the range in the middle of a loop". This is the case where Liquid Types help, tremendously. But such complicated cases, where Liquid Types shines, may not fit into a talk. Again, it is not fair to think this is a complication specific to Haskell.
- CyberDildonics 3y ago
  Again, it is not fair to think this is a complication specific to Haskell. It is fair, because other languages have a single keyword or setting instead of a whole 'type system' with fancy labels that introduces lots of complexity for something simple.
  - one-punch 3y ago
    It is not fair to think this is a complication specific to Haskell, because you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia, with functions such as unsafeTake and unsafeDrop. https://news.ycombinator.com/item?id=37382215 https://news.ycombinator.com/item?id=37382215 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. https://news.ycombinator.com/item?id=37387005 https://news.ycombinator.com/item?id=37387005 It is unfair to not respond to these points, while calling "this is a complication specific to Haskell." Because Haskell can do what others can do, but more. > lots of complexity for something simple. "indexing an array of length 8" for parsing UDP headers is simple, agreed. And Haskell can handle that simply with unsafe functions. Keeping track of properties with complicated dependencies to parse arbitrary content (perhaps application-logic-aware contents, not "just checking for array length before indexing in a loop") is simple, strong disagree. See the section "Beyond Bounds Checking" of "Why Liquid Haskell matters" for example [1]. This might be used to implement the kinds of static analysis needed for Mojo or Swift, for instance [2]. [1]: https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ "Why Liquid Haskell matters" [2]: https://github.com/modularml/mojo/discussions/466 https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism" https://news.ycombinator.com/item?id=37376010 https://news.ycombinator.com/item?id=37376010 And this cannot be solved in the languages you mentioned, either. Unless you are claiming that all parsing checks are "just checking for array length before indexing in a loop". https://news.ycombinator.com/item?id=37416911 https://news.ycombinator.com/item?id=37416911 We are still working on completely different scales. The talk is using a toy example to show what is possible, and you are using that example too literally, without realizing that the example scales to handle much more complex problems that people need to deal with in the real world. It is unfair to lump together different scales and call them the same thing. Your reaction is like criticizing a talk which shows sorting 5 numbers with programs, with "it is simple to sort 5 numbers by hand, why bother learning how to program with all those complexity for something this simple?". And then calling this fair, without realizing that in the real world, sometimes people need to sort way more than 5 numbers.