Follow

My first attempt in trying Liquid has been an epic failure.

):

@otini @pureevil I ended up having two problems.

First one was Liquid Haskell complaining about non terminating recursion, for “trivial” structural recursion (e.g. for a Tree datatype).

Second one was a strange bug with smtlib2. To be honest, I used the liquid haskell master so this might be a reason, I probably should have used a tag version.

@lthms I see. Annoying… did you end up temporarily leaving it aside?

@pureevil

@otini @pureevil yeah. I will probably come back to it eventually, since I am really interested in investing Liquid Haskell proof-related features. But I also have to have a look at F* so…

(so many things to investigate)

@lthms @otini @pureevil F* was a lot of fun to use when I looked at it last a couple years ago. A very fast moving thing where the meta-theory isn't pinned down, which is both exciting and scary. It might have calmed down since.

Sign in to participate in the conversation
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!