Mastodawn

Lindsey Kuper Mar 19

I've gotten like four emails now from a professor in France who watches my distributed systems videos. The most recent one, today: "With time passing, I came a fan of your class on distributed systems CSE138. It is an amazing work, and I am recommanding it to my students as a class very consistent with what we are teaching. Also your american is slow and very understandable, so it is also a reason to listen your videos !"

My American is slow and very understandable 👍

Questions he's asked me:

- can he use one of my blog posts to help design an exam? (yes)
- does Liquid Haskell have any particular support for reasoning about physical time? (nope)
- are the sequence numbers used by Paxos the same thing as Lamport clocks? (not quite)
- do I have a video on Chord? (not specifically, but I have one on consistent hashing)

I love this guy

Shae Erisson Mar 19

@lindsey I have one correspondent on the internet who randomly messaged me, and I have the same feelings for that person!

[off topic]
They were looking for deep understanding of how to run ten year old hardware[1] and I was the only person they could track down to ask!

[1] IBM QS20 blades (Cell Broadband Engine) in an IBM BladeCenter

@lindsey What would "reasoning about physical time" look like? Is there a PL that allows that?

Lindsey Kuper Mar 19

@bool Well, some languages have a more or less "native" notion of "time", which might or might not correspond particularly closely to physical time. There's stuff like the ChucK language, but I honestly don't really understand it!

Lindsey Kuper Mar 19

@bool In my research group (cc: @Twisol), we've studied abstractions that preserve key aspects of physical time, like the notion of causality. You could have a programming language in which causality-violating programs cannot be expressed.

Lindsey Kuper Mar 19

@bool @Twisol But real time is continuous (or...seems to be, anyway? I dunno, you'd have to ask a physicist), and so it seems like we can talk about real time with computers only to the extent that we can talk about continuous data with computers. And that is really not something I know much about!

@lindsey Thank you, it sounds very interesting

ShadSterling Mar 19

@lindsey @bool @Twisol (IIRC, if time is quantized, the quanta are no larger than the Planck Time, and it’s not expected to be possible to directly test for quantization at smaller scales. Some theories, including variants of String Theory, hypothesize quantized time, but AFAIK no methods for experimentally testing any of those theories have yet been devised)

ShadSterling Mar 19

@lindsey @bool @Twisol (We’ve begun to be able to investigate the process of the photoelectric effect - rather than treating it as an instantaneous change - without getting close to the Planck Time limit. So yeah, for every demonstrable purpose, time is continuous)

ShadSterling Mar 19

@lindsey @bool @Twisol since I first read about efforts to make software timing predictable or controllable I’ve found it fascinating that processors seem to be the human-made machines with the most consistent timing for the most repetitions, both by a huge margin, but despite that we don’t know how to make software that runs with consistent timing.

(Unless maybe there’s a known way in realtime embedded systems that I haven’t read about yet?)

Ted Mielczarek Mar 19

@lindsey @bool would it be fair to read "physical time" as like "unix timestamps" or something similar?
I'm not familiar with the distributed systems side of things but Rust, for example, has a distinction between `std::time::Instant`, an opaque monotonically-increasing timer from which you can calculate durations, and `std::time::SystemTime`, which is basically "a timestamp I got from elsewhere" (e.g. the filesystem).

Lindsey Kuper Mar 19

@tedmielczarek @bool yeah, various languages have standard library functions that provide access to some monotonic clock source provided by the OS. I think that's what `std::time::Instant` is; I wasn't thinking of it as a language-level concept.

RSNikhil Mar 20

@bool @lindsey If you consider digital clocks as a proxy for physical time then, yes, there are some "synchronous PLs" (Signal, Lustre, Esterel) and there is SVA (SystemVerilog Assertions, a temporal logic) that enable reasoning about time.

Ruchira S. Datta Mar 19

@lindsey Is "physical time" different than what's considered in temporal logics or in model checking? Is it that he cares about the wall-clock reading?

It's said that implementing GPS required relativistic corrections. I have no idea how specifically these were implemented.

Lindsey Kuper Mar 19

@RuchiraSDatta I don't know; "physical time" is my paraphrase of what he asked me. Here's an actual quote from his email: "Is liquid Haskell able to take time into account (dealines, time intervals) ?"

Liquid Haskell has no particular support for "tak[ing] time into account" in the way that it seems like he's looking for.