Hacker News new | ask | show | jobs
by temp123789246 1349 days ago
Out of curiosity, does anyone know how this compares to something like Liquid Haskell? Is one more or less powerful than the other?
1 comments

The two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT solver to check if assertions hold.

From what I have seen LH focuses on integrating into the type system (it is Liquid as in the 2008 Liquid Types paper). Generally it is possible to rewrite properties attached to a type to contracts, e.g. a non-zero Int input becomes a precondition that says that argument is non-zero. Checking termination with Prusti is also something we are working on.