Re: Tesla Coils Corpses report: programming language design
As far as we can see the vast majority of things that people write are trivially terminating, or they have an infinite loop based on I/O. You might want to look up co-recursion and codata, a way to deal with I/O based infinite loops, and still keep some notion of totality and (co-) termination. See eg http://blog.sigfpe.com/2007/07/data-and-codata.html?m=1 On Fri, 19 Dec 2014 08:17 Zooko Wilcox-OHearn zo...@leastauthority.com wrote: [Folks: the weekly “Tesla Coils Corpses” meetings are, by design, not limited to any particular topic, or to any practical requirements. We let out imaginations fly free! This week, our imaginations flew into new programming languages…] Tahoe-LAFS Tesla Coils Corpses, 2014-12-18 in attendance: Daira, Zooko (scribe), Za (briefly), Graydon Hoare Unifying types and values. A singleton type is, for example, a type representing a single value, such as 3, instead of representing a domain of values, such as the type int32. (A domain is a generalization of a set. Domain theory works by having a partial order on the information that you have about a value, and elements of a domain are limits of a sequence of values that are each giving you more information.) Abstract interpretation is where you compute all possible results from some given information about the inputs. It is the generalization of constant computation in current normal programming languages. You can obviously do abstract interpretation using types. Let's say you have a range type of the integers from A‥B. (Let's use the convention that this is inclusive of A and exclusive of B.) So we can have A‥B + C‥D = (A+C)‥(B+D). Aside: much of Rust's region-memory-management system is copied from Cyclone. A lot of the improvement is easing the cognitive and notational burden and making the error messages helpful. Dependent types. In most languages the value space and the type space are completely separate, so you have expressions involving values and expressions involving types and they are completely separate. You can have annotations which combine those two spaces by saying that a value is of a given type, but you can't say that this type depends on this value. One of the reasons why dependent type systems haven't caught on is the perceived complexity between these two levels, one of which depends on the other. There's this set of type systems called pure type systems which try to simplify this by unifying certain constructs that appear both at the value level and at the type level. A Π-type is, you can think of it as a function from values to types, although it is part of the type language and so strictly speaking not a function. The basic idea is that you compute using singleton types. So you're treating normal computation as a special case of abstract computation. If you do that then you don't actually need the value level. Or equivalently you don't need the type level. You just need one. Q: Aren't there going to be some things that are going to be intractable with abstract interpretation? Well, you need only to compute approximations. Abstract interpretation is in general only ever computing approximations. For example, suppose you have an if statement, and you want to compute an approximation of the possible outputs, taking into account both cases of the if, so you run the program abstractly through both branches of the if and then take the union of the results. Graydon says C++ has dependent types, but people use it for very little. This sort of programming is trying to see into the future and define invariants that will hold through all time. In Graydon's experience, people can't see very far. Daira's theory, which might turn out to be wrong, is that the clunkiness is part of the problem. Graydon agrees that better notation can let the user see further. Daira is hopeful that if we reduce the impedance mismatch between the value and the type language — ideally by making them identical — then it will be easier to incrementally make the types more precise. For example, by writing QuickCheck-style checks, and then converting them into proofs. Graydon says that the incrementalism is interesting. The layering, stratification, and incrementalism in the design of Noether is interesting to him. Most systems today, says, Graydon, assume that you want all of the machinery turned on all the time. Most proof assistants are not useful for mucking around — you can use it if you know what theorem you want to prove, but if you don't them you can't do anything, can't even write Hello world. ACL2 is an exception to that pattern. Noether uses the effects system to specify which sublanguage a given function is in. That's actually really important to making it tractable, both cognitively and in terms of the type system. You can specify that certain functions are total. Graydon was worried that
Re: Tesla Coils Corpses report: programming language design
On 18 December 2014 at 21:17, Zooko Wilcox-OHearn zo...@leastauthority.com wrote: You can obviously do abstract interpretation using types. Let's say you have a range type of the integers from A‥B. (Let's use the convention that this is inclusive of A and exclusive of B.) So we can have A‥B + C‥D = (A+C)‥(B+D). Surely (A+C)..(B+D-1). Including B would've made it easier :-) ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
Tahoe on AWS
Hi, I'm trying to set up a system of 1 introducer and 10 storage nodes on AWS, plus one client on my laptop. The introducer sets up, but when I run it, the introducer.furl always reflects the internal IP that AWS assigns and not the public IP. Is there a way around this? Also, apart from port 3456 TCP, what ports do I need to open on the introducer and the storage nodes? cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
Re: Tahoe on AWS
Hi Sameer, You need to set (in the node section) the tub.location configuration parameter. Here's the details: https://tahoe-lafs.org/trac/tahoe-lafs/browser/docs/configuration.rst And... if you are in San Francisco then come to by Tahoe-LAFS cryptoparty tomorrow night at noisebridge! https://www.cryptoparty.in/sanfrancisco Cheers, David Stainton On Fri, Dec 19, 2014 at 3:21 AM, Sameer Verma sve...@sfsu.edu wrote: Hi, I'm trying to set up a system of 1 introducer and 10 storage nodes on AWS, plus one client on my laptop. The introducer sets up, but when I run it, the introducer.furl always reflects the internal IP that AWS assigns and not the public IP. Is there a way around this? Also, apart from port 3456 TCP, what ports do I need to open on the introducer and the storage nodes? cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
Re: Tahoe on AWS
On Thu, Dec 18, 2014 at 7:30 PM, David Stainton dstainton...@gmail.com wrote: Hi Sameer, You need to set (in the node section) the tub.location configuration parameter. Here's the details: https://tahoe-lafs.org/trac/tahoe-lafs/browser/docs/configuration.rst Thanks! And... if you are in San Francisco then come to by Tahoe-LAFS cryptoparty tomorrow night at noisebridge! https://www.cryptoparty.in/sanfrancisco Oh sweet! I'll reschedule some stuff and try to be there. cheers, Sameer Cheers, David Stainton On Fri, Dec 19, 2014 at 3:21 AM, Sameer Verma sve...@sfsu.edu wrote: Hi, I'm trying to set up a system of 1 introducer and 10 storage nodes on AWS, plus one client on my laptop. The introducer sets up, but when I run it, the introducer.furl always reflects the internal IP that AWS assigns and not the public IP. Is there a way around this? Also, apart from port 3456 TCP, what ports do I need to open on the introducer and the storage nodes? cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
Re: Tahoe on AWS
On Thu, Dec 18, 2014 at 8:27 PM, Sameer Verma sve...@sfsu.edu wrote: On Thu, Dec 18, 2014 at 7:30 PM, David Stainton dstainton...@gmail.com wrote: Hi Sameer, You need to set (in the node section) the tub.location configuration parameter. Here's the details: https://tahoe-lafs.org/trac/tahoe-lafs/browser/docs/configuration.rst Am I setting the tub.location for both introducer and storage servers? I have my introducer running (green) but storage servers show as red saying Connected to 0 of 3 known storage servers cheers, Sameer Thanks! And... if you are in San Francisco then come to by Tahoe-LAFS cryptoparty tomorrow night at noisebridge! https://www.cryptoparty.in/sanfrancisco Oh sweet! I'll reschedule some stuff and try to be there. cheers, Sameer Cheers, David Stainton On Fri, Dec 19, 2014 at 3:21 AM, Sameer Verma sve...@sfsu.edu wrote: Hi, I'm trying to set up a system of 1 introducer and 10 storage nodes on AWS, plus one client on my laptop. The introducer sets up, but when I run it, the introducer.furl always reflects the internal IP that AWS assigns and not the public IP. Is there a way around this? Also, apart from port 3456 TCP, what ports do I need to open on the introducer and the storage nodes? cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
juju charm for tahoe-lafs
Is anyone aware of juju charms for tahoe-lafs, especially for running storage servers on AWS or OpenStack? Juju: https://jujucharms.com/ cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
Re: Tahoe on AWS
On Thu, Dec 18, 2014 at 9:11 PM, Sameer Verma sve...@sfsu.edu wrote: On Thu, Dec 18, 2014 at 8:27 PM, Sameer Verma sve...@sfsu.edu wrote: On Thu, Dec 18, 2014 at 7:30 PM, David Stainton dstainton...@gmail.com wrote: Hi Sameer, You need to set (in the node section) the tub.location configuration parameter. Here's the details: https://tahoe-lafs.org/trac/tahoe-lafs/browser/docs/configuration.rst Am I setting the tub.location for both introducer and storage servers? I have my introducer running (green) but storage servers show as red saying Connected to 0 of 3 known storage servers Never mind. I got it. I changed the tub.port and tub.location on the storage servers and it shows up as green now. Sameer cheers, Sameer Thanks! And... if you are in San Francisco then come to by Tahoe-LAFS cryptoparty tomorrow night at noisebridge! https://www.cryptoparty.in/sanfrancisco Oh sweet! I'll reschedule some stuff and try to be there. cheers, Sameer Cheers, David Stainton On Fri, Dec 19, 2014 at 3:21 AM, Sameer Verma sve...@sfsu.edu wrote: Hi, I'm trying to set up a system of 1 introducer and 10 storage nodes on AWS, plus one client on my laptop. The introducer sets up, but when I run it, the introducer.furl always reflects the internal IP that AWS assigns and not the public IP. Is there a way around this? Also, apart from port 3456 TCP, what ports do I need to open on the introducer and the storage nodes? cheers, Sameer ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev ___ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
