Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Liquid Haskell: Haskell as a Theorem Prover [pdf]

goto.ucsd.edu

Post reply on HN
Print view View original

21–28 of 28 posts

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#21

Post by nikivazou »

bbcbasic wrote: post #6

Is this providing a similar purpose to say code contracts in .NET? Albeit I am sure this is more comprehensive.

It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only express things that the SMT solvers can decide fast (eg linear arithmetic). So, checking will definitely terminate and it will terminate fast.

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#23

Post by nikivazou »

xvilka wrote: post #22

What the difference with Agda? Why not it?

Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means that with Liquid Haskell your verified code can use general language features, such as exceptions, diverging code, parallelism and all the Haskell optimized libraries.

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#24

Post by namarkiv »

alokedesai wrote: post #14

This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq ( https://coq.inria.fr/ ) being one of the most famous ones.

I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance.

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#25

Post by namarkiv »

xvilka wrote: post #22

What the difference with Agda? Why not it?

While you can write verified programs in agda, and use the MAlonzo FFI to extract haskell code, the generated code is very inefficient. On the other hand, this lets you write proofs in Haskell that coexist with your program, so there's little to no impact on runtime performance.

Also, Agda is an implementation of Martin-Lof type theory, which is very, very different from what SMT is.

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#26

Post by aninhumer »

wildmusings wrote: post #20
acomar wrote: post #13

Earlier quoted context omitted.

Thanks! This has me down a rabbit-hole because I'm now trying to find the name for a related concept: once you've learned a new idea/model, you start to notice how it applies to everything around you. I find this happening most often with algebraic ideas but the article you linked alludes to the fact that you're liable to notice this effect at play more in the days after reading about it. I want to call it overfittin…

This is the Law of the Instrument: if all you have is a hammer, then everything looks like a nail.

I don't think that's really the same meaning. Here it's more like, if you're given a hammer, you'll notice a lot of nails you can use more easily now.

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#27

Post by xvilka »

nikivazou wrote: post #23
xvilka wrote: post #22

What the difference with Agda? Why not it?

Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means that with Liquid Haskell your verified code can use general language features, such as exceptions, diverging code, parallelism and all the Haskell optimized libraries.

Thank you for your explanation and writing this. Added in my todo list to play with. I understand this one is the official repo: https://github.com/ucsd-progsys/liquidhaskell ?

Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]

#28

Post by mkawa »

If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis:

http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf

The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques.

[1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf

[2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.p...

[3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf

[4] https://www.microsoft.com/en-us/research/wp-content/uploads/...

[5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf

Post reply on HN