dlab IRC 2017 October 22nd

Next day: 2017-10-23

#dlab logs for 2017-10-22

rawles (Simon Rawles) (new topic)
[11:12:12Z] A distributed laboratory. Everything which appears here is logged.
adamfc (Adam Forsythe-Cheasley)
[13:15:18Z] hello
[13:54:49Z] afternoon!
[14:04:52Z] I've invited Tim here so too.
[14:06:07Z] -so
[17:45:52Z] Today I'm implementing a basic dependency manager in Java, which allows you to define expressions and variables, then when one variable is changed, so are the ones it depends on, automatically. Like in a spreadsheet.
[18:22:19Z] oh interesting
[18:22:29Z] so the dependencies are anything?
[18:22:49Z] i.e. are they objects?
[18:23:57Z] So a dependency is 'a is b + c'. The variable a is dependent on b and c, and takes the value b + c. When either b or c change, a changes too.
[18:24:24Z] ah ok
[18:24:42Z] I could have just put '=', but that suggests assignment in programming to me.
[18:25:01Z] I've got a big plan for this, but this is the ground work.
[18:25:02Z] yeah
[18:26:19Z] Do you have a project right now?
[18:32:10Z] not really
[18:32:28Z] I was reading a bit more about homotopy type theory
[18:32:36Z] I guess that was the closest thing to a project recently
[18:32:42Z] it was interesting
[18:32:53Z] esp. in the fact that you could build up everything from it
[18:33:11Z] and it's essentially spaces
[18:33:33Z] I keep meaning to read the PDF book that Adam linked to and put it on my Kindle - https://homotopytypetheory.org/book/
[18:33:34Z] which reminded me of an idea you were talking about where you were representing logical statements as spaces
[18:33:48Z] oh I forgot he linked to a book
[18:34:04Z] from his post at https://cp4space.wordpress.com/2017/10/02/homotopy-type-theory/
[18:34:24Z] oh this is good, you can just read the book for free
[18:34:44Z] There's some order theory in there, so I should really take the time to look at it! What do you find interesting about it?
[18:35:09Z] Is there anything you could do with it, like a programming project?
[18:35:19Z] I guess at the moment I find it interesting that it's *not* set theory
[18:35:32Z] but I guess also that it's easier to encode
[18:35:40Z] so you can have a computer check a proof
[18:35:43Z] that's quite interesting
[18:36:14Z] I think people are working on a framework and a language with homotopy type theory as the basis
[18:36:16Z] The book I was reading ages ago was http://www.cambridge.org/gb/academic/subjects/computer-science/programming-languages-and-applied-logic/topology-logic?format=PB&isbn=9780521576512
[18:37:19Z] Like a programming language?
[18:37:37Z] https://coq.inria.fr/
[18:37:50Z] 'a formal proof management system'
[18:39:29Z] I've heard of Coq but never looked very deep into it. This seems interesting.
[18:39:55Z] Right, that's on my reading list then.
[18:41:03Z] Oh, it's in OCaml too.
[18:41:09Z] yeah, I was just seeing that
[18:41:17Z] have you done much OCaml?
[18:42:10Z] No, but there are lots of fans of it among the programmers we know in Bristol.
[18:43:39Z] oh right
[18:56:48Z] Have you?
[18:56:57Z] I don't know anything about it really
[20:21:45Z] I've not looked at it, no
[21:16:54Z] Luke, a friend of Rick's, posted this: https://fine-disregard.blogspot.co.uk/2017/10/digits-in-powers-of-2.html
[21:18:15Z] Let f(n) denote the number of digits of n (in base 10) that are greater than or equal to 5 (so f(128) = 1, f(1024) = 0 and f(1048576) = 4). What is the sum of f(2^k)/(2^k) (from k = 0 to infinity)?

All timestamps are in UTC. If you want to join in, channel information is available. This page is generated from raw logfile dlab-2017-10-22-000000.txt.