Fork me on GitHub
#off-topic
<
2019-11-22
>
Cameron06:11:52

OH @sogaiu I didn't even recognize you, you're in the Arcadia chat too right

Cameron06:11:31

I thought your name looked familiar

Cameron06:11:42

ok, so I guess that means I did recognize you .. but you get it ahahaha

π 4
jaihindhreddy06:11:52

I've been wondering whether space-time is continuous, and from whatever little research is done, it seems like the science hasn't settled yet, but evidence points towards it being continuous.

sogaiu14:11:56

wondered similarly off and on. no resolution, but fun thoughts come about. e.g. perhaps continuity is actually an approximation method that happens to work well when things are actually discrete, but the numbers involved are vast.

jaihindhreddy06:11:09

What does that do to the epochal time model?

jaihindhreddy06:11:58

Is the epochal time model then saying, regardless of whatever the physical nature of space-time might be, us humans can only work on epochs and so it makes sense to model time in our programs this way?

henrik09:11:23

Small enough epochs are effectively continuous. Regardless of the actual nature of things, itβs probably going to be keep being fine to model time as epochal.

π― 4
jaihindhreddy09:11:14

Yup. That's what I was thinking. Epochal model is good more because humans work that way than reality being that way.

jaihindhreddy11:11:12

After watching the conj talk about `piggy`, I now see some of what Rich Hickey meant in questioning the way spec does function specification. Lemme explain using the same example as in the talk: Let's say we are writing `+`, and have said, "give me some integers and I'll give you an integer back", and then later wanted our function to also work with floats, saying "give me some numbers and I'll give you a number back", despite being accretion, cannot be proven so because we weakened our promise of returning an integer to now returning a number. Spec-checking code cannot understand the fact that, if I call + with integers, I will get back an integer. Parameterized types will make this easier, but won't account for mixed types. We want to be able to say "the input is a sequence of numbers" but also say, "if you give me only integers, then I'll give you an integer, but if there is one of more floats in the arguments, then you'll get a float back". This becomes even more complicated with ratios involved.

jaihindhreddy11:11:18

I have no idea what the answer is.

jaihindhreddy11:11:17

I also remember Rich saying something like: "So do not go crazy if you cannot completely spec the entire nature of your inner algorithm, because sometimes it is challenging." Maybe I am going too far and hoping spec will become some sort of compatibility-proving system. What do y'all think?

jaihindhreddy11:11:40

Sorry for being this verbose. I couldn't put it any better.

andy.fingerhut11:11:45

I am not sure what you mean by "despite being accretion, cannot be proven". If you mean, "cannot be proven automatically by a proof tool that exists today", then agreed. If you mean "cannot be proven in any way at all, in principle", then I don't see why you say that.

π 4
jaihindhreddy13:11:52

Yes. Automatic was what I meant. I was thinking if a specification system that can, given two spec'ced fns, old and new, guarantee that new won't break old. But after some more thinking, I feel "guarantee" is a strong word, and will come down to the halting problem.

andy.fingerhut14:11:42

If a spec does not use user-defined functions, then I am pretty sure it is a decidable problem. Rich Hickey mentioned the decidability of the problem "is regular expression A a subset of regular expression B?" in early talks on Clojure spec as a reason for using regular expressions in spec.

andy.fingerhut14:11:04

Granted that lots of interesting specs do use user-defined functions, and then things get undecidable very easily.

β 4
andy.fingerhut14:11:29

They certainly get much much more difficult to recognize the decidable ones in an automated proof tool.

π― 4
phreed00:11:33

you picked a well known problem involving extension of the category of integers to reals. With a conversion function βcβ from reals to integers and the natural transformation c(r1) + c(r2) = c(r1 + r2) we have the essentials for our proof.

4
andy.fingerhut11:11:40

It seems that someone who knew the implementation of + well enough could prove that if you give it only integers, it returns an integer (or bigint).

andy.fingerhut11:11:59

It also seems that if you did want to go crazy writing precise function specs, you could spec + to return a value satisfying int? if all of its arguments satisfied int?, else if there was at least one ratio in the args, then return ratio, else if there was at least one double in the args, return double, etc.

borkdude11:11:18

Off topic. What I noted: there usually was some Twitter Clojure drama just a few weeks before the conj a few years in a row. This year I didn't notice such a thing (which is good of course). I wonder if something has changed. Maybe the people who were dissatisfied have now left, or more transparancy through Alex's blogs have helped give more insight in what Cognitect is doing at the moment and where their priorities are.

borkdude12:11:34

Anyway, happy things seem to be going smoothly right now.

andy.fingerhut12:11:04

Or the timing of the drama was coincidental?

borkdude12:11:10

Could totally be.

borkdude12:11:45

Maybe Autumn/Winter also makes people more vulnerable to moodiness and Twitter drama

Mno12:11:42

Well the cold makes them stay indoors more, and reduced social interaction plus more time on a computer will increase the chances of being on twitter in a not so great mood.

Mno12:11:05

I want to see if this idea holds true statistically for all things on twitter.. :thinking_face:

borkdude15:11:21

Does anyone has a nice setup for this? You have a PC at home (linux, or Windows) and want remote desktop access on your laptop (in my case Macbook) no matter where you are (so has to work outside of home). What software do you use for this?

borkdude15:11:15

I could maybe use https://www.zerotier.com/ for this, no idea if it's fast enough for remote desktop type of work

sogaiu15:11:32

too paranoid to try these things π i think another direction is to put stuff remotely to begin with.

borkdude15:11:20

> to put stuff remotely to begin with

borkdude15:11:24

how do you mean this?

sogaiu15:11:08

iiuc, you want access to certain computing facilities no matter where you are. for some situations, putting those facilities in a data-center (or equivalent, e.g. linode, paperspace, etc.) to begin with means you don't put your home network at as much risk. may be it doesn't work for your situation though.

borkdude15:11:43

it's for development

borkdude15:11:58

I just want to develop like I do on my laptop but with more resources

sogaiu16:11:51

i can relate -- i don't have access to one of my dev machines right now π

Do you want Remote Desktop or just shell access?

Personally, I have found that Windows has much better remote desktop support than mac.

Self-hostable Remote Desktop tooling https://guacamole.apache.org/

borkdude16:11:46

preferably the entire desktop, not only shell

borkdude16:11:20

π 4

let us know if you find anything that works for you @U04V15CAJ! The only remote desktop I use these days is TeamViewer to support my parentsβ mac (free for non commercial use).

borkdude16:11:24

I also use that for my parents π. I haven't actually bought a PC yet, but I'm just looking for options

dharrigan16:11:46

@U04V15CAJ zerotier ftw! I use it extensively I also use wireguard too

borkdude16:11:10

@U11EL3P9U Is zerotier fast enough for a remote desktop connection over the internets?

dharrigan16:11:30

I've used it for VNC into my mac (when I need it) - without any discernable difference

dharrigan16:11:59

But, I would lean towards wireguard - I have absolutely no metrics or emperical evidence to support this, but wireguard feels a bit quicker.

dharrigan16:11:44

It's been a while 'tho since I need my mac for anything, since all my dev and day-to-day stuff happens on Linux π

dharrigan16:11:23

Weill be interesting to evaluate ZeroTier 2.0 when out next year.

sogaiu16:11:14

perhaps the speed of something is going to depend on one's specific location?

borkdude16:11:18

I've used ZeroTier before and it worked well, but I haven't used it with loads of data

dharrigan16:11:44

@sogaiu absolutely - so many factors π

borkdude16:11:28

of course, but let's assume the wifi I'm at is fast and my home's internet connection is also fast (500 mbit up/down)

borkdude16:11:39

what's in the middle, I have no idea generally

sogaiu16:11:43

i guess if things involved don't use any 3rd party one should be able to compare the speeds directly

sogaiu16:11:16

@U11EL3P9U thanks for mentioning wireguard, hadn't heard of it π

dharrigan16:11:30

you'r welcome π It's pretty neat π

borkdude16:11:01

is wireguard as easy to setup as zerotier? I found the latter pretty convenient

borkdude16:11:13

also zerotier works on macos

dharrigan16:11:14

It's probably about the same IMHO.

dharrigan16:11:20

Wireguard too

dharrigan16:11:28

I use Wireguard on mac as well.

dharrigan16:11:33

It's on the app store π

sogaiu16:11:41

it's nice that both have at least some bits as source

borkdude16:11:44

ooh fancy π

borkdude16:11:40

ssh / shell access is probably a lot gentler on data usage, so that may be the first approach

+1 for Wireguard. I run my own VPN servers on Digital Ocean and itβs speedy. As far as hosting a Wireguard server at home: I already use Home Assistant and Wireguard is available as an add-on in http://hass.io https://community.home-assistant.io/t/community-hass-io-add-on-wireguard/134662

@U04V15CAJ, the last time I tried to remote desktop to a mac for work was a few years ago. I did not have a speedy internet connection like you do. I found VNC based solutions too sluggish and at the time hunted around for an RDP solution, and (I think) I settled on iRAAP (now out of business). If you want to try an RDP host solution you might dig into https://www.nuords.com (note that I've not tried this one).

borkdude19:11:36

Ah, Mac only though

oh you want linux or windows...

windows has great RDP support built in

borkdude19:11:17

Well, buying a PC for extra resources is much cheaper than a Mac Pro

borkdude19:11:47

it's still hypothetical, but some of the work in the company I work for is very RAM hungry

sogaiu19:11:35

i agree with lread that the remote stuff (for desktop access) tends to be better for windows these days -- mac has not steadily improved here in my experience. i use xfreerdp to access a windows box from *nix.

borkdude19:11:46

nice. that would also get me a box to test any weird GraalVM issues π

I think Microsoft has an RDP client for macOS... if you are connecting from mac to windows.

jaide19:11:45

Contemplating trying out https://shadow.tech/usen/ for remote windows gaming from my mac. They offer iOS, Android, and Desktop apps to access machines and it is access to a decked out windows machine.

sogaiu19:11:34

i also see paperspace mentioned often when shadow is -- haven't really tried either

borkdude19:11:56

that's connecting to some cloud gaming box?

sogaiu19:11:40

iiuc, there is a gaming option, but there is (or used to be) an option to just connect to a box which you can do other things with

sogaiu19:11:24

borkdude19:11:38

interesting, but I bet that's going to be costly as a permanent solution

sogaiu19:11:39

paying as you go seemed attractive to some folks

sogaiu19:11:01

could be -- i think it could really depend a lot on details

sogaiu19:11:38

when you go with the hosted option, you don't control the fine details of hardware, but may get upgrades down the line and can pay for more or less sometimes as your needs change. you don't have to worry as much about hardware obsolence, security, etc. i think it really depends.

sogaiu19:11:14

having said all of that i like having my own boxes π

jaide20:11:18

@U04V15CAJ It's a full windows box so you could do gaming, which is probably the broadest market to appeal to but I've heard accounts of people using it for CPU intensive tasks like video editing. I find the price compelling as you get a pretty decent machine for less than the initial build cost and it gets upgraded over time. However, I haven't pulled the trigger yet.

borkdude20:11:31

Interesting developments

futuro21:11:20

(From a security perspective, using a VPN to connect to your home network lets you open ports on your home machine without having to expose it to random access)

borkdude21:11:04

Yes, VPN or ZeroTier + RDP software seems a good combo

rory22:11:50

Good old fashioned X forwarding over an SSH tunnel?

futuro22:11:03

Once youβre inside your home network, yeah, but opening an ssh port to your desktop means you need to harden it against attack. Setting up a vpn already has certain hardness guarantees, and putting it on a raspberry pi reduces the attack surface.