Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-11-01

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
10:19 ilbot3 joined #isabelle
10:19 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
12:31 bitraten joined #isabelle
18:00 cheater joined #isabelle
18:00 cheater hi
18:01 cheater is isabelle/hol a good system to work with modules as "objects" that I would like to check the properties of?
18:02 cheater e.g. if i have multiple modules connected together in various ways, I would like to make sure that changing the property of some sub module will not break other things in the network
18:02 cheater I'm guessing this is somehow related to bigraphs, but I haven't studied bigraphs enough to say
18:05 anders0 i don't see why not
18:12 cheater anders0: i don't know proof systems that well yet, I'm just a simple Haskell programmer. Maybe you could help me figure out if the following is difficult to do? I would like to define modules with properties. Modules have inputs and outputs and can be stuck together. This is to describe an infrastructure of servers. I wonder if I could somehow depict transitivity of properties. Say I have a web ...
18:12 cheater ... server that can store and display records in a database. If the database provides data durability, then so does the web server. However if the db suddenly is changed to not provide durability, the web server itself would not provide durability on its own. Hence the compound module of "web server+db" wouldn't either. Is there a way to somehow reason about such things? Is it difficult?
18:12 cheater oh, I also studied maths, so I know about axioms, proofs, and such
18:15 cheater it would be best if i could then use the properties i've defined to generate code for Haskell or Scala (type signatures)
18:15 anders0 it sounds like you just need to change "durable web_server" to "durable db --> durable web_server" or something, in this case.
18:15 anders0 anyway, yeah, you can generate haskell/(oca)ml/scala code from isabelle
18:16 cheater anders0: that implication is exactly what i want
18:16 cheater anders0: what would the code look like there? (i'm not familiar with the syntax yet, but i've seen some isabelle code and it looked fairly natural)
18:17 anders0 say you have durable :: "server => bool", and implication is just "==>"
18:18 anders0 if you've ever used a dependently-typed language for modelling something, isabelle might seem weirdly simple
18:18 anders0 like, just manipulating functions "something => bool"
18:18 cheater i've never used dependent types
18:18 anders0 oh, never mind then :)
18:18 cheater i realize isabelle/hol doesn't have dependent types
18:20 cheater anders0: so i'd do durable :: "server => bool"; "durable db ==> durable web_server";
18:20 cheater how would i pose that the db is durable, and to check if web_server is durable?
18:22 anders0 hmm
18:23 anders0 are you trying to prove that the server implementations provide data durability?
18:24 anders0 or just, if they do, then [some other nice property]
18:26 cheater i'm just trying to prove this simple property of durability
18:27 cheater so a server is a thing that hooks up to a db, and provides durability if the db provides durability
18:27 cheater and then i say: i have my web server, and my specific db, say pgsqldb, provides durability. the question is: does web_server provide durability?
18:28 cheater then I change to another db, say mongodb, which does not provide durability, and now I ask again whether web_server provides durability.
18:29 anders0 i see
18:31 anders0 to be honest, i'm not really sure, short of reimplementing part of the server in isabelle (or taking some properties just on trust)
18:31 anders0 i'm hoping someone else will chime in soon with an easier way to do it :p
18:33 anders0 if you do have to do that, though, then haskabelle might make it a little less of a hassle (assuming it's a haskell program)
18:36 anders0 this AFP entry might be relevant too, though i haven't read through it: http://afp.sourceforge.net/entries/ComponentDependencies.shtml
18:37 cheater anders0: i take properties just on trust
18:37 cheater anders0: how would i take properties on trust?
18:37 cheater i mean the only property i need to know about the web_server is "durable db ==> durable web_server"
18:37 cheater maybe i can use a more easier maths example
18:38 cheater say i have a function f of one argument
18:38 anders0 i mean that when you come to prove that, you'll need to know "something" about how the web server acts
18:38 cheater f : X -> Y
18:38 cheater f has the property that if it is passed an even x, then the y it spits out is also even
18:38 cheater now i pose that a is even
18:38 cheater how do i ask isabelle whether f(a) is even?
18:39 cheater how do i describe this problem in isabelle?
18:39 anders0 fun f :: "nat => nat" where (*definition*)
18:40 anders0 darn, that was supposed to be a newline
18:40 anders0 lemma f_even: "even n ==> even (f n) (* proof *)
18:41 anders0 then when you need the fact that f preserves evenness you just refer to f_even
18:42 cheater anders0: i don't know the definition of f
18:42 cheater i just know that if x is even, then f(x) is even
18:42 anders0 right
18:42 cheater there is no proof, i just assume this
18:43 cheater it's been proven on paper or something like that
18:43 anders0 ok, so whenever you need to know that, then you add "even n ==> even (f n)" as an assumption
18:43 cheater hmm
18:44 anders0 you can also add it as an axiom, but i suspect that's probably considered bad practice
18:45 cheater not sure what the difference is between an axiom and an assumption
18:46 anders0 by an assumption i mean the P and Q in a proposition like "[P; Q] ==> R", and by assumption i mean something you've claimed is globally true
18:47 anders0 (or P∧Q → R in normal notation)
18:48 cheater i think by the second "assumption" you meant "axiom"
18:48 cheater but anyways
18:48 cheater i wanted to ask two other things if you still have the time..
18:48 anders0 uh, yeah, sorry
18:48 anders0 sure. but i'm far from an isabelle expert myself :)
18:48 cheater if i'm on ubuntu, and normally use vim for my editing, what's the best way to install and use isabelle?
18:48 cheater and the second one was
18:49 cheater can i use isabelle/hol as a companion to the HoTT book?
18:51 anders0 unfortunately, jedit's the only supported way to write in isabelle, since it's really unpleasant to do without the live "here is the current goal" business
18:51 anders0 (there used to be an emacs frontend too, but it's not supported in isabelle2014)
18:53 anders0 as for HoTT: i have no idea, sorry. :) maybe someone's already started to formalise it somewhere
18:55 anders0 since it uses a dependent type theory, it probably doesn't fit into HOL that well, but it might be possible to do as a separate logical system
18:56 anders0 (i don't actually know: HOL has separate worlds for types & terms, but I'm not sure if it's possible to write a logic in isabelle which doesn't)
18:57 anders0 wait, what am i talking about! you could do it just fine, as long as you don't need the HoTT types to be at the isabelle type level
18:58 anders0 sorry. yes, you could do it fine, i think. :B
18:59 anders0 i still don't know of an existing one, but if you're following the book you'd probably want to do it yourself anyway.
19:00 cheater oh
19:00 cheater that makes sense
19:03 anders0 there are ones for coq and agda, according to this google search, but those both *do* use dependent types which is IMO somewhat different in feel
19:06 cheater yeah i know of coq and agda
19:20 cheater anders0: thanks a lot for your help
19:20 cheater anders0: that's really nice of you to jump in like that
19:41 anders0 no problem :D i wish i was more experienced in isabelle so i could give more detailed answers
19:51 cheater i think that was great though, thanks :)
20:16 cheater joined #isabelle
21:40 cheater__ joined #isabelle
22:00 cheater__ joined #isabelle
22:42 cheater__ joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary