Our great sponsors
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
> C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out.
Haskell can do that too, with unsafeTake and unsafeDrop [1], you can opt-out of runtime bounds checks like C++, Rust, and Julia. But opting-out of machine-checked guarantees is unsafe.
The extra thing is that Liquid Haskell can move such runtime bounds checks to compile time, made ergonomic with SMT solvers. This way, you get machine-checked guarantees (so programmers can write correct programs faster) with no runtime overhead (the programs also run faster).
> Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from.
Yes, that's the whole point of static analysis, to move runtime checks to compile time, made ergonomic with Liquid Types. Note that this compile time verification is much stronger than testing at development time (which is what C++, Rust, and Julia offer without Liquid Types).
> That should be something that is prevented ahead of time, not recovered from.
Gabriella Gonzalez agrees with you, and calls this idea of "Prefer pushing fixes upstream over pushing problems downstream" as "The golden rule of programming", at the 1st slide in her talk [2].
[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Documented preconditions - Scrap your Bounds Checks with Liquid Haskell"
[2]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
For a concrete example of Liquid Haskell, see how Gabriella Gonzalez safely removed bound checks of high-performance protocol parsing, in "Scrap your Bounds Checks with Liquid Haskell" [1].
With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. With static types, programmers can write correct programs faster, and the programs also run faster.
As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2].
[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
[2]: https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"