Liquid Haskell

[dolio]

I was told a few years ago that someone had created a modified version of vector-algorithms that used Liquid Haskell to demonstrate index safety (I believe) of the algorithms. I always thought it would be cool to pull in this work, and make it something that could be run like a test suite. But I never got around to inquiring about it.

I assume this would be a very difficult project, because some of the current algorithms post-date the proofs, and even some of the ones that would be covered have probably changed some. I also don't know much about Liquid Haskell myself, so I can't say how difficult it would be to cover the remaining algorithms or fix any problems in the old proofs.

I'm also not sure what to make of the fact that there were still index problems in some of the old algorithms that were presumably shown safe.

If someone comes along who is interested in this project, I can probably provide introductions to the right people to see if it's still feasible.