“…The conjecture that I pose is that many of the properties that would usually require dependent types to ensure at compile time, can be described in Liquid Haskell specifications. …”

This conjecture, I hope is true. And it could very well apply to anything from Janet, to Pascal, to Python or Typescript.

There are seems to be two views on what the type system is for (I am sure, i am simplifying here bit too much):

a) it is a compiler hint for how to translate the intent of the programmer to machine (including the intent of a lifecycle for a variable)

b) it is a compiler hint for how to evaluate the correct usage of the variable (or a collection of variables) of a given type throughout the code

Some programming languages adapted (a) and are slowly switching to incorporate (b). eg. C++ Some languages adopted (b) from the start, and work on adapting (a).

But if I follow the above conjecture, why these two views should be ‘incorporated’ into a single type system . Why not keep that separate, and have essentially 2 type systems expressed differently through out the program.

Which examples of real-world Liquid Haskell libraries exist on Hackage?