monochrom 2017-03-04 07:45:19
The wrong-specification problem is solved by not assigning blames unilaterally. You only assert "implementation mismatches specification". You don't assert the assymetric "implementation is wrong". The value of verification is that you now get two perspectives (the implementation and the specification) not just one (the implementation), this is supposed to be more informative.
ertes 2017-03-04 07:45:56
also changing assumptions can be quite expensive
ertes 2017-03-04 07:46:10
up to completely having to redo all proofs
rly 2017-03-04 07:46:59
ertes: if you write a program without a proof, you still need to do that work, except you don't write it out and you hope for the best.
ertes 2017-03-04 07:47:41
rly: you don't need to, and generally it's not done
rly 2017-03-04 07:47:56
ertes: sure, and that's why all bug trackers are filled.
cocreature 2017-03-04 07:48:20
so let's just stop using computers because writing correct software is impossible
ertes 2017-03-04 07:48:26
try to look for formal proofs in the linux kernel… not machine-checked proofs, just formal ones that would actually count as real proofs, i.e. instances of "you still need to do that work"
johnw 2017-03-04 07:48:32
cocreature: it's not impossible, just hard
ertes 2017-03-04 07:48:42
rly: it's easy to say: "it needs to be done"
ertes 2017-03-04 07:48:46
actually doing it is a different story
cocreature 2017-03-04 07:48:46
johnw: I was being sarcastic :)
monochrom 2017-03-04 07:48:54
I do stop exercising because it is hard. :)
monochrom 2017-03-04 07:49:43
Also, I stopped demanding proofs of correctness because getting people to write proofs is hard.
monochrom 2017-03-04 07:50:05
Writing proofs is not hard for me. But getting other people to do it is hard.
ertes 2017-03-04 07:50:15
one factor is that our tools aren't adequate for formalising a whole system
rly 2017-03-04 07:50:18
I think the problem is that there are only a few people on the planet who can write proofs and not all of those teach.
ertes 2017-03-04 07:50:32
and i believe before they get adequate, AI will take over writing them
rly 2017-03-04 07:50:39
I.e., write proofs of "production quality".
ertes 2017-03-04 07:51:07
rly: that's *a* problem… a more relevant problem is that it's *hard*, even for people who can do it
MarcelineVQ 2017-03-04 07:51:07
monochrom: where do you learn to write proofs?
rly 2017-03-04 07:51:33
ertes: part of the reason is that proving theorems is in EXP.
rly 2017-03-04 07:51:39
ertes: so, of course it is hard.
MarcelineVQ 2017-03-04 07:51:41
monochrom: would sicp teach me?
monochrom 2017-03-04 07:52:03
And it doesn't have to be proofs. You need to wipe-clean your keyboard? Guess what, doing it yourself is so much easier than convincing someone else to do it.
rly 2017-03-04 07:52:15
monochrom: haha
cocreature 2017-03-04 07:52:16
MarcelineVQ: software foundations is pretty good if you are interested in formalizing and proving things about software
ertes 2017-03-04 07:52:34
rly: now combine that with the problem of practical/commercial feasibility… sure, software is never *finished*, but at some point you want to produce something people can actually use =)
rly 2017-03-04 07:53:05
ertes: lots of software I have written happily hums away in data centers/clouds.
cocreature 2017-03-04 07:53:17
in a lot of cases the cost of bugs is simply cheaper than the cost of verifying that there are no bugs
ertes 2017-03-04 07:53:18
rly: and those are formally verified?
rly 2017-03-04 07:53:25
ertes: I wrote them, so they are perfect ;)
ertes 2017-03-04 07:53:30
so no
rly 2017-03-04 07:54:12
ertes: the only reason I am interested in formal tools, is because I don't like the quality of the software the rest of the planet is producing.
rly 2017-03-04 07:54:43
ertes: the current software development process doesn't scale for > SMALL_CONSTANT number of people.
rly 2017-03-04 07:55:04
The Linux kernel solved it by using trust.
MarcelineVQ 2017-03-04 07:55:04
I'm quite interetsed in learning about this stuff. even the idea of a proof is a little bit of black magic to me, if something works for x+1 and x+2 how can you then know it works for x+n
cocreature 2017-03-04 07:55:22
MarcelineVQ: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html that's the book I was mentioning
ertes 2017-03-04 07:55:23
MarcelineVQ: induction
monochrom 2017-03-04 07:55:25
MarcelineVQ: Bird's textbooks are one kind of books that teach proofs.
monochrom 2017-03-04 07:55:35
I haven't read SICP.
ertes 2017-03-04 07:55:53
MarcelineVQ: you prove that 1. it works for 0, 2. if it works for x, it also works for x + 1, for all x
cocreature 2017-03-04 07:55:59
I've read the first half or so of sicp. I don't think it helps with teaching proofs
ertes 2017-03-04 07:56:18
MarcelineVQ: then in a certain sense magically it works for all natural numbers =)
cocreature 2017-03-04 07:56:41
induction on natural numbers made a lot more sense to me once I saw general structural induction and understood that natural numbers are just a special case of that
ertes 2017-03-04 07:56:50
(induction is not universally accepted as a valid principle, but i think most mathematicians accept it)
monochrom 2017-03-04 07:57:03
Induction is explained poorly because most explainers do not make explicit the "forall" quantifiers.
rly 2017-03-04 07:57:30
Induction is something you learn in high school.
monochrom 2017-03-04 07:57:58
You rightfully observe that "(forall x. works for x) => (forall x. works for x+1)" is circular logic. But induction does not say that.
monochrom 2017-03-04 07:58:26
Induction says "(forall x. (works for x => works for x+1))". Very different.
monochrom 2017-03-04 07:59:24
Once upon a time, there was a kid who saw a wounded bird. The kid was kind-hearted and able, he saved the bird and healed it.
monochrom 2017-03-04 07:59:45
The bird turns out to be a fairy. The fairy says, "I will grant you two wishes".
ertes 2017-03-04 07:59:59
MarcelineVQ: exercise: prove that the sum of two even natural numbers is an even natural number… you may use the usual arithmetic properties (associativity, distributivity, etc.) of addition and multiplication
Fairy 2017-03-04 07:59:59
I said no such thing!
monochrom 2017-03-04 08:00:02
(Why two, why no three? Because I'm teaching induction!)
monochrom 2017-03-04 08:00:15
Haha OK sorry Fairy. Different fairy.
Fairy 2017-03-04 08:00:20
<_<
monochrom 2017-03-04 08:00:45
The kid was a math geek. (I guess the fairy was, too.) So he said: first wish, today I receive one gold coin.
monochrom 2017-03-04 08:01:35
Second wish: For each day, if I received a gold coin on that day, then I will also receive a gold coin on the next day.
monochrom 2017-03-04 08:02:06
If you now see that the kid will receive everyday a gold coin thereafter, you have understood induction.
ertes 2017-03-04 08:03:19
then the fairy says: "sorry, i'm propositional, but i'm happy to serve your first wish"
buttons840 2017-03-04 08:05:12
while were on this topic -- i was wondering if dependant types can be used to prove anything which is true? i know there are certain types of logic that cannot be expressed with dependant types, but are there alternative proofs for the same things?
MarcelineVQ 2017-03-04 08:05:48
ertes: I don't know what it means to prove something ^^; uhm, 2 + 2 = 4 this is true regardless of which two is in which spot, why is this true, well, uhm, 1 + 1 is 2, 2 + 1 + 1 is 4 1 + 1 + 2 = 4 and even 1 + 1 + 1 + 1 = 4
ertes 2017-03-04 08:06:38
MarcelineVQ: first define what it means for a natural number to be even
ertes 2017-03-04 08:06:52
MarcelineVQ: use the phrase "there exists" in your definition
buttons840 2017-03-04 08:07:46
MarcelineVQ: i am reading a book called "How To Prove It", which is focused on mathematical proofs and not on any computer program, but it might be a good resource for you to learn about proofs
doyougnu 2017-03-04 08:08:43
You may want to checkout Proofs in Idris then. 2 + 2 = 4 in Idris looks like this:
doyougnu 2017-03-04 08:08:43
two_plus_two : n = 2 -> m = 2 -> m + n = 4
doyougnu 2017-03-04 08:08:44
two_plus_two p q = rewrite p in rewrite q in Refl
MarcelineVQ 2017-03-04 08:11:10
there exists a set of natural numbers which consists only of multiples of 2, they are called even numbers
ertes 2017-03-04 08:11:48
MarcelineVQ: definition: for all natural numbers n the statement "n is even" is equivalent to the statement: there exists …
ertes 2017-03-04 08:11:54
finish the sentence
osa1 2017-03-04 08:13:55
what's wrong with this pattern synonym: `pattern Some x <- Left x where Some x = Left x` ?
ertes 2017-03-04 08:14:46
MarcelineVQ: if you can't figure it out: why is 10 even? what makes it even?
cocreature 2017-03-04 08:15:00
osa1: compiles for me, what makes you think it is incorrect?
osa1 2017-03-04 08:15:19
cocreature: I get an error
osa1 2017-03-04 08:15:27
ghc 8.0.1
cocreature 2017-03-04 08:16:05
osa1: hm works with 8.0.2 and 8.0.1 for me
osa1 2017-03-04 08:16:10
huh, 8.0.2 doesn't give an error
MarcelineVQ 2017-03-04 08:16:10
there exists a factor of 2?
ertes 2017-03-04 08:16:24
MarcelineVQ: yeah… 10 is even, because it's a multiple of 2
ertes 2017-03-04 08:16:42
and "multiple of 2" means: "there exists a natural number k such that 10 = 2*k"
ertes 2017-03-04 08:17:40
MarcelineVQ: now generalise this: definition: for all naturals n, "n is even" is the same statement as: there exists …
osa1 2017-03-04 08:17:50
cocreature: http://lpaste.net/353216
geekosaur 2017-03-04 08:18:38
osa1, iirc 8.0.1 does have some bugs in patsyns
geekosaur 2017-03-04 08:18:47
you may want to stick to 8.0.2
cocreature 2017-03-04 08:18:53
osa1: that's different to the one you pasted here. it uses Right and not Left in the constructor
xubunto 2017-03-04 08:19:34
jw what does lift do?
xubunto 2017-03-04 08:19:47
(i assume haskell has this function)
osa1 2017-03-04 08:19:50
cocreature: ahh! so can't I use Right in the pattern part and Left in the expression part?
cocreature 2017-03-04 08:20:13
osa1: it definitely feels wrong but I'm still thinking about why that's not allowed :)
ertes 2017-03-04 08:20:20
xubunto: it's most likely 'lift' from MonadTrans… do you have a working understanding of monads?
osa1 2017-03-04 08:20:29
yeah it's weird but it should be possible
xubunto 2017-03-04 08:20:36
ertes: yes
ertes 2017-03-04 08:21:11
xubunto: let T be a monad transformer, then 'lift' embeds an action of the target monad m in (T m)
ertes 2017-03-04 08:21:15
lift :: m a -> T m a
MarcelineVQ 2017-03-04 08:21:23
it feels a bit like parroting, but: there exists a natural number k such that n = 2*k
ertes 2017-03-04 08:22:05
MarcelineVQ: that's correct, and it may feel like it, but having a precise definition in terms of logical primitives (in this case: explicit quantification) is important
xubunto 2017-03-04 08:22:29
MarcelineVQ: is that lifting too?
cocreature 2017-03-04 08:22:54
osa1: ah! it works with an explicit type signature. so it's just ghc's inference that is not smart enough to figure out that the left and right side have to have the same type
ertes 2017-03-04 08:22:59
MarcelineVQ: now try to prove that the sum of two even naturals is always an even natural… first formulate an actual logical statement, a precise version of this statement
xubunto 2017-03-04 08:23:04
oh
ertes 2017-03-04 08:23:09
MarcelineVQ: you will need the phrase "for all"
osa1 2017-03-04 08:23:19
cocreature: how do you add a type sig to a pat syn?
ertes 2017-03-04 08:23:29
MarcelineVQ: (you may reuse your definition of "even" now, because now it's exact)
ertes 2017-03-04 08:23:42
((taking the definition of naturals for granted))
cocreature 2017-03-04 08:23:54
osa1: http://lpaste.net/353217
xubunto 2017-03-04 08:23:55
ertes: so say i lift just 5
tsahyt 2017-03-04 08:24:04
Is there such a thing as an applicative transformer?
ertes 2017-03-04 08:24:08
xubunto: lift (Just 5)
xubunto 2017-03-04 08:24:19
what would that do
ertes 2017-03-04 08:24:22
tsahyt: sure, every monad transformer is an applicative transformer
tsahyt 2017-03-04 08:24:31
ertes: but what about transformers for things that are applicatives but not monads?
osa1 2017-03-04 08:24:33
cocreature: awesome! thanks
ertes 2017-03-04 08:24:33
tsahyt: but there are easier methods to combine applicative functors
ertes 2017-03-04 08:24:52
xubunto: lift :: Maybe a -> T (Maybe a)
ertes 2017-03-04 08:25:02
xubunto: choose T, then it may be clearer what it means
ertes 2017-03-04 08:25:19
whoops
ertes 2017-03-04 08:25:22
xubunto: lift :: Maybe a -> T Maybe a
xubunto 2017-03-04 08:25:55
ertes: either *2 or String
ertes 2017-03-04 08:26:07
xubunto: do you know what MaybeT is?
newbie64 2017-03-04 08:26:14
hi, what is the difference between polytypic programming and generic programming?
tsahyt 2017-03-04 08:26:16
ertes: what I'm dealing with here is that I have values that are calculated recursively with an ArrowLoop interface (which does make more sense here than for FRP) and a 1 sample delay on each recursive step. But this of course can lead to infinite recursion quite quickly. So I was thinking about providing a type that provides limited recursion somehow, since that's how you generally handle these things in
tsahyt 2017-03-04 08:26:18
DSP
xubunto 2017-03-04 08:26:34
ertes: no
ertes 2017-03-04 08:27:00
xubunto: newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }
ertes 2017-03-04 08:27:14
for all monads m, (MaybeT m) is a monad
ertes 2017-03-04 08:27:24
in other words: instance (Monad m) => Monad (MaybeT m)
ertes 2017-03-04 08:27:49
xubunto: you may want to take it as an exercise to implement Functor, Applicative and Monad instances for this by yourself
kuribas 2017-03-04 08:28:14
Strange how adding code makes it faster... I added an iteration limit, and my code is 25% faster!
ertes 2017-03-04 08:28:22
xubunto: once you've done that, implement the following instance: instance MonadTrans MaybeT
xubunto 2017-03-04 08:28:36
i went through the stuff for functors
ertes 2017-03-04 08:28:37
this will require you to implement 'lift' for MaybeT
kuribas 2017-03-04 08:28:38
Probably has something to do with cache prediction...
glguy 2017-03-04 08:29:55
lolisa: Assuming polytypic means definitions using polymorphic types, the definitions are implemented with no knowledge of the type variables, and specific knowledge of the non-type variables. so 'map :: (a -> b) -> [a] -> [b]' is going to work uniformly in choices of 'a' and 'b', using only the knowledge of lists and functions
glguy 2017-03-04 08:30:40
lolisa: Typically "generic" programming is where the structure of the function definition gets access to the structure of the types its operating on without being tied to a specific type
glguy 2017-03-04 08:30:47
This happens using Template Haskell, GHC.Generics, or SYB/Data.Data
glguy 2017-03-04 08:31:17
where the structure of types is made available either in a common type representation or a common value representation
lolisa 2017-03-04 08:31:45
Sorry... I should provide some context
lolisa 2017-03-04 08:32:07
http://www.cs.ox.ac.uk/ralf.hinze/talks/Nijmegen.pdf
glguy 2017-03-04 08:32:33
Did you have a more complete question then?
lolisa 2017-03-04 08:33:49
Yes. Polytypic programming also 'look into constructor' so it seems very similar to generic programming. I dont know if they are the same thing, or have some subtle difference.
glguy 2017-03-04 08:34:18
Into a specific constructor
glguy 2017-03-04 08:34:49
Like for map, only the constructors (:) and [] are available, not those of types 'a' or 'b'
MarcelineVQ 2017-03-04 08:36:31
ertes: for all even natural numbers n and for all even natural numbers k, n+k is even
lolisa 2017-03-04 08:37:02
I think polytypic is not the same thing as polymorphic...
xubunto 2017-03-04 08:37:46
ertes: ill look into applicative functors
glguy 2017-03-04 08:38:38
lolisa: Yeah, this talk appears to use polytypic to mean what I described as generic
ertes 2017-03-04 08:38:38
MarcelineVQ: yeah… can you prove it? show why it must be true
glguy 2017-03-04 08:38:51
paper->slides
lolisa 2017-03-04 08:39:31
thx anyway :)
lolisa 2017-03-04 08:39:57
ertes, yes. induction on the definition of eveness.
glguy 2017-03-04 08:40:11
lolisa: This looks like the precursor to GHC.Generics
lolisa 2017-03-04 08:40:34
Yes it sure does. Very interested into such thing.
lolisa 2017-03-04 08:40:48
to be more formal, induction on the proof that n is a even number.
lolisa 2017-03-04 08:41:09
base case: n = 0 is a even number, n + k = 0 + k = k, use the other hypothesis
ertes 2017-03-04 08:41:35
lolisa: please don't spoil it… it's an exercise!
jle` 2017-03-04 08:41:55
i have my types defined in a seperate 'types' file, but in order to write instances for it, i would be using some utility functions that aren't defined in the types file
lolisa 2017-03-04 08:41:56
Oh, very sorry, does not see context
jle` 2017-03-04 08:42:08
if i move them all to the types file then the file becomes a bit bloaded and it sort of defeats the purpose
glguy 2017-03-04 08:42:18
Related to GHC.Generics, I did an implementation of a unified lens/traversal generator supporting type-changes this week http://lpaste.net/353157
jle` 2017-03-04 08:42:19
is there any common strategy to handle this nicely?
ertes 2017-03-04 08:42:31
(also you don't need induction here… i explicitly allowed MarcelineVQ to use arithmetic properties of addition and multiplication)
cocreature 2017-03-04 08:42:46
jle`: I sometimes have a Types.Util module
glguy 2017-03-04 08:43:03
Don't merge all the types into a Types file?
xubunto 2017-03-04 08:43:29
ertes: can you give me a direction on applicative functors? (i have a sense on normal functors)
jle` 2017-03-04 08:43:40
glguy: but if i don't do that then i end up with cyclic imports eventually usually
jle` 2017-03-04 08:43:51
cocreature: does types.util have the typeclass instances too?
cocreature 2017-03-04 08:44:20
jle`: depends, I don't have strict rules here
glguy 2017-03-04 08:44:26
jle`: That's OK, you can make hs-boot files so that you can maintain the complicated types in separate modules and still have them import each other where needed
