mbrock 2017-02-23 10:45:52
or, well, even manual formal proving (Agda checks proofs automatically but writing them isn't very automatic)
thatguy 2017-02-23 10:46:03
is is actually of practical use at the moment for proving new unknown stuff or is it a theoretical field?
thatguy 2017-02-23 10:46:19
I know the logicians at my university are doing that kind of stuff but I myself have no experience
mbrock 2017-02-23 10:47:03
automated logic for verifying systems in a broad sense is very practical, for example chip manufacturers do it on huge scales to verify the correctness of CPUs and stuff (I have no experience with this)
mbrock 2017-02-23 10:48:06
but that's mostly not with dependent type languages and stuff, it's different formalisms more based on simple logic
thatguy 2017-02-23 10:48:46
ah I can imagine that
cocreature 2017-02-23 10:50:18
thatguy: http://www.nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990 is one example of fully automated proofs
thatguy 2017-02-23 10:51:29
cocreature, thanks! I'll read it after my haskell practice session
mbrock 2017-02-23 10:51:46
at the moment I have a somewhat simple program that still ends up having many possible states. There are important properties of this program that I want to be sure of (and that I want others to be able to be sure of), and I can actually verify many such properties in quite a nice way using QuickCheck
mbrock 2017-02-23 10:52:38
QuickCheck is like proofs for lazy people: you give a theorem that you hope holds, and the tool just checks it for N random inputs
thoughtpolice 2017-02-23 10:52:44
This is a very good book on automated theorem proving: http://www.cl.cam.ac.uk/~jrh13/atp/. The author works at Intel on FPU verification. ATP is very popular in those areas, yes.
thoughtpolice 2017-02-23 10:53:21
And yes, it's often vastly easier. If you just want to "Upgrade" your QuickCheck properties to real proofs, I suggest something like Liquid Haskell. It's highly automated.
monochrom 2017-02-23 10:53:59
I love John Harrison.
dmwit 2017-02-23 10:54:19
Tuplanolla: Yes. Generally the reasoning is `const NotErased`, which really sucks, but there's plenty of research papers looking into how to do a good job of it.
mbrock 2017-02-23 10:54:55
but when the input starts to have lots of structure, it becomes harder to make sure that your arbitrary input generator generates relevant test cases, so you start to feel that even though 1000 test cases passed, maybe they just didn't trigger the relevant code paths
monochrom 2017-02-23 10:55:13
He actually theorem-prover'ed floating-point algorithms for sqrt sine etc for his PhD
thoughtpolice 2017-02-23 10:55:13
monochrom: It's a fantastic book. I wish he would write another.
mbrock 2017-02-23 10:55:13
so that's happening to me and it's making me want to just explicitly prove some of these properties
Tuplanolla 2017-02-23 10:55:13
That's interesting, dmwit. I've only written proofs with dt, so I haven't encountered these problems.
mbrock 2017-02-23 10:55:38
thoughtpolice: thanks for the recommendation, I will definitely see what Liquid Haskell can do in my case. It basically checks properties with an SMT solver, right?
monochrom 2017-02-23 10:56:13
He still maintains HOL-Light. And what he put into HOL-Light inspired improvements to HOL4.
thoughtpolice 2017-02-23 10:56:30
mbrock: Correct. The trick is being able to phrase things correctly in such a way the solver can reasonably find a solution. Sometimes this is tricky but for a lot of things, it's not bad.
monochrom 2017-02-23 10:56:41
I.e. the HOL4 people learned much about ease-of-use from him.
shapr 2017-02-23 10:57:40
Is there something like gopacket / scapy /etc for Haskell?
thoughtpolice 2017-02-23 10:57:42
Liquid Haskell also now allows explicit theorem proving, so you can use it as the hard-mode escape hatch, for lemmas or proofs of things that are not easily automated.
thoughtpolice 2017-02-23 10:59:06
monochrom: I haven't used HOL4, but I largely followed the code in his book and used HOL-Light. I've wanted to write a Haskell port of it for a while, now.
thoughtpolice 2017-02-23 10:59:40
HOL-Light proofs are often surprisingly nice to read IMO. The backtick quasiquoting works well for low 'overhead'.
mbrock 2017-02-23 11:00:14
oh, interesting. I experimented a tiny bit with the z3 SMT solver (using sbv), but I got scared when I realized that one of my core functions involves taking an arbitrary fixed point number to an arbitrary integer power (often large), which seems like quite a degenerate case of nonlinear arithmetic
mbrock 2017-02-23 11:01:23
which makes me think I will need to put in some lemmas...
mbrock 2017-02-23 11:01:31
(I'm super new to all this stuff)
dmwit 2017-02-23 11:01:38
mbrock: sbv may be able to do that for bounded exponents, but yeah I don't think it will be able to touch that on unbounded exponents.
thoughtpolice 2017-02-23 11:01:43
mbrock: Well, in that case, it's going to be difficult. You really are trying to quantify over arbitrary exponents, so yes, that's hard. I had similar kinds of issues but in my case I was able to relatively easily rephrase them.
thoughtpolice 2017-02-23 11:01:55
Z3 can do certain forms of nonlinear arithmetic, it's awesome like that. But yes that's a tricky one.
mbrock 2017-02-23 11:02:25
I could probably just limit it to 1000 or whatever
monochrom 2017-02-23 11:02:26
thoughtpolice: The backtick quasiquoting is an important feature of ML that is missing in Haskell. You will have an uphill battle because of this.
dmwit 2017-02-23 11:02:39
mbrock: http://hackage.haskell.org/package/sbv-5.15/docs/Data-SBV.html#g:20
thoughtpolice 2017-02-23 11:02:55
IIRC in my case I wanted to quantify over some inequality over 'any given sized bit integer' which was tricky. Instead I rephrased it as a property about an integer which is a simple numeric property that can later be constraint solved. This is a lot simpler.
mbrock 2017-02-23 11:05:29
dmwit: yeah, I'm gonna have to give that thing a try again :)
thoughtpolice 2017-02-23 11:05:57
monochrom: Yes, phrasing the UI is what is tricky. You either implement a full on parser and quasiquote whole blocks, or you quasiquote almost every other expression. Or you can do an eDSL directly, which comes with all its own problems.
monochrom 2017-02-23 11:09:06
thoughtpolice: http://www.mail-archive.com/haskell-cafe@haskell.org/msg09203.html :)
mbrock 2017-02-23 11:13:38
I wonder if I will run into trouble using LiquidHaskell on a program that's full of TH-generated record field lenses and whatnot
mbrock 2017-02-23 11:14:28
or probably because it works on Core it will be fine
pikajude 2017-02-23 11:14:52
Why does stack install a GHC when the correct version is already in scope?
pikajude 2017-02-23 11:15:36
hmm
pikajude 2017-02-23 11:15:39
maybe my assumption is incorrect
Koterpillar 2017-02-23 11:16:07
pikajude: you have to allow system GHC explicitly
pikajude 2017-02-23 11:16:12
how do I do that?
Koterpillar 2017-02-23 11:17:31
system-ghc: true
Cale 2017-02-23 11:17:36
mbrock: Is LiquidHaskell actually practical to run on anything which is of nontrivial length now?
Koterpillar 2017-02-23 11:17:37
in ~/.stack/config.yaml
Koterpillar 2017-02-23 11:17:47
pikajude: also see compiler-check
pikajude 2017-02-23 11:18:18
ok
pikajude 2017-02-23 11:18:22
thanks
shapr 2017-02-23 11:19:29
I wonder if a bunch of neat lenses on top of network-house would give me a friendly packet editing framework in Haskell?
mbrock 2017-02-23 11:23:35
Cale: ah, I have no idea. My program isn't huge, but kind of just past non-trivial
kadoban 2017-02-23 11:35:11
mbrock: Probably some DRM thing?
mbrock 2017-02-23 11:35:17
yep
