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

11–20 of 28 posts

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

#11

Post by jeff_marshall »

airesQ wrote: post #5

There is an interactive tutorial at [1]. I find this quite amazing. With refinement types one can say/prove things like: - This function only returns even numbers. - The input for this function is not just any vector, it must be an ordered vector. - It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type s…

There have been quite a few systems that can handle proofs of the kinds of propositions you list above using various different logical frameworks, programming languages, and automatic and/or user-guided proof assistants.

That said, it's no small feat to do a correct translation from the semantics of a full, modern, programming language into the semantics of a SMT solver (which appears to be the primary back-end for deciding propositions in this tool). I'll have to go read the actual dissertation to see how far that goes and whether any escape-hatches for user guidance exist (tactics, manual term manipulation, etc.). I haven't yet found a tool that doesn't allow extensive user guidance to be all that effective for proving things about code/systems that are interesting (to me).

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

#12

Post by eveningcoffee »

DanGarcia595 wrote: post #2

I find this delightfully coincidental that the very moment I found this I was sitting in AI class as my professor stresses the usefulness of a good automated theorem prover.

It would be interesting to know what were your professor arguments and what was suggested as a better solution.

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

#13

Post by acomar »

ShaneWilton wrote: post #9
acomar wrote: post #7

Earlier quoted context omitted.

I do too. I suspect they're a form of confirmation bias, however, because it's not easy to remember that you heard about an idea or term you're unfamiliar with. On the other hand, something you've just recently heard or learned stands out: it reinforces the lesson you've just learned.

You'd probably be interested in this article about the phenomenon: https://www.damninteresting.com/the-baader-meinhof-phenomeno...

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 overfitting but that's not quite right.

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

#15

Post by platz »

bbcbasic wrote: post #6

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

liquid haskell (refinement types) is similar to F* https://www.fstar-lang.org/ which exports code to .Net (and OCaml)

I think because Code Contracts are not utiling any form of Dependent Types (i.e. refinement types), there is only so much that it can statically check/enforce. Refinement Types can go much farther, and their whole utility is in static checks, not runtime checks/unit tests.

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

#17

Post by pizza »

curiousgal wrote: post #4
DanGarcia595 wrote: post #2

I find this delightfully coincidental that the very moment I found this I was sitting in AI class as my professor stresses the usefulness of a good automated theorem prover.

Offtopic but I absolutely love it when those "delightful coincidences" or synchronicities occur. Examples also include me learning about something right before someone else brings it up.

https://en.wikipedia.org/wiki/Coincidence_detection_in_neuro...

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

#18

Post by transposed »

acomar wrote: post #7
curiousgal wrote: post #4

Earlier quoted context omitted.

Offtopic but I absolutely love it when those "delightful coincidences" or synchronicities occur. Examples also include me learning about something right before someone else brings it up.

I do too. I suspect they're a form of confirmation bias, however, because it's not easy to remember that you heard about an idea or term you're unfamiliar with. On the other hand, something you've just recently heard or learned stands out: it reinforces the lesson you've just learned.

Once you've learned a thing, or "studied it" much more, you are more swift in perceiving it, processing, and storing that encounter. Be it an idea, name, combination of low frequency words... Otherwise, many things go in one ear and out the other.

What really gives me the goose bumps is if you're, say, listening to a recording of a lecture while looking out the window watching a leaf tumble through the wind - and then the professor uses a leaf blowing in the wind analogy. It's not something you do very frequently; watch and listen to two independent events.

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

#19

Post by bbcbasic »

The very first blogpost http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... gives a very nice jargon and maths-free introduction to this. You don't need to know Haskell to follow it really.

The assert function shown in the post is really cool. Amazing how easy it is to define a function that will compile time check an assertion (e.g. something is not "null"). That's code contracts done in the 101 class.

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

#20

Post by wildmusings »

acomar wrote: post #13
ShaneWilton wrote: post #9

Earlier quoted context omitted.

You'd probably be interested in this article about the phenomenon: https://www.damninteresting.com/the-baader-meinhof-phenomeno...

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.
Post reply on HN