Liquid Haskell: Haskell as a Theorem Prover [pdf]
goto.ucsd.edu
Liquid Haskell: Haskell as a Theorem Prover [pdf]
1–10 of 28 posts
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#2I 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.
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#3Talk by Niki Vazou, the author of the dissertation: https://www.youtube.com/watch?v=LEsEME7JwEE
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#4I 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.
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#5There 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 saying that the function must always evaluate to true. The theorem prover does the rest.
[1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logi...
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#6Is this providing a similar purpose to say code contracts in .NET?
Albeit I am sure this is more comprehensive.
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#7I 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.
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.
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#8Earlier 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.
>something you've just recently heard or learned stands out
Not only does it stand out, at times it seems to appear more frequent. I found out that was called the Baader-Meinhof Phenomenon.
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#9Earlier 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.
You'd probably be interested in this article about the phenomenon: https://www.damninteresting.com/the-baader-meinhof-phenomeno...
Re: Liquid Haskell: Haskell as a Theorem Prover [pdf]
#10Earlier 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.
[deleted]