DSys RG Oct 2022: Edelweiss

Paper

Video

Chat Log

00:09:24	Sodium :	the thing where they're figuring out what data will *never* get used feels like looking for places where data falls out of the "computational light-cone" or something
00:22:04	quinn:	But usually in static analysis w/ Datalog you're working with total lattices, which might be what you're thinking about
00:24:47	Sodium :	katara: https://arxiv.org/abs/2205.12425 https://github.com/hydro-project/katara (crdt synthesis from C++ with some annotation)
00:28:43	Sodium :	What if mass storage were free? https://dl.acm.org/doi/pdf/10.1145/1013881.802685
00:32:46	Sodium :	was mildly amused by the "left as an exercise to the reader"-lite of
> The procedure for deciding to move to a new epoch is orthogonal to this program; a common approach is to use a separate (and more expensive) protocol based on distributed consensus [9, 33]
00:33:17	Philipp Krüger:	:100:
00:33:18	Philipp Krüger:	:D
00:33:53	aesakamar:	✋
00:35:35	Marc-Antoine Parent:	I agree with the criticism. Automating the “optimizations” makes sense, but the results must be shown to the user for validation
00:35:39	Philipp Krüger:	Yeah - imagine writing programs that would normally loop infinitely, but rely on the compiler optimizing them such that they don't
00:36:38	Marc-Antoine Parent:	But I agree with the declarative approach otherwise
00:38:12	Marc-Antoine Parent:	Interesting that katara went for annotations instead of high-level declarative
00:38:45	Sodium :	that felt like a practical/pragmatic choice i think. both because LLVM already exists, and because people already have C++ code
00:39:16	Sodium :	better adoption with annotations vs A Whole New Language imo (e.g. typescript's whole deal)
00:39:41	Marc-Antoine Parent:	oth typescript adoption is quite good :-)
00:41:06	Sodium :	a distsys language with `unsafe`-equivalent blocks
00:41:49	quinn:	Bloom actually kinda has that! You can write code that needs coordination: BUT Bloom will tell you when you do that so that it isn't done by accident
00:43:22	quinn:	Oh and here's "Abstracting Geniuses Away from Failure Testing": https://cacm.acm.org/magazines/2018/1/223887-abstracting-the-geniuses-away-from-failure-testing
00:43:37	quinn:	"It relies on the superuser's ability to interpret how a distributed system employs redundancy to mask or ameliorate faults and, moreover, the ability to recognize the insufficiencies in those redundancies—in other words, human genius."
00:45:09	aesakamar:	Unison ❤️
00:45:32	quinn:	Unison is very cool 😄 Philipp (in the call) has written some neat Unison demos
00:45:59	Philipp Krüger:	Well, I met aesa for the first time at unisonforall (he gave a talk), soooo :D
00:46:00	quinn:	Hole-driven development for distributed systems?
00:46:14	Sodium :	https://www.unison-lang.org/ for the curious
00:46:56	Brooklyn Zelenka (@expede):	Ah, right! IIRC that was recorded — Aesa or Philipp can you post a link to the talk?
00:47:29	Philipp Krüger:	https://www.youtube.com/watch?v=rOO2gtkoZ3M
00:47:51	quinn:	Yeah. Aesa, you fit right in here :P
00:48:08	Sodium :	🧡 dependent types
00:48:52	quinn:	I like fanciful ideas
00:49:57	Zeeshan Lakhani:	I’m very anti dependent types for user oriented programming :), except for doing proofs directly.
00:50:10	Sodium :	"Depending on Types - Stephanie Weirich" https://www.youtube.com/watch?v=n-b1PYbRUOY
00:51:23	quinn:	💯
00:51:57	Sodium :	dependent type stuff feels like it's still extremely in its infancy UX-wise imo. it feels like there's a possible future dependent types situation exists that *doesn't* suck or break your wrists to write
00:53:22	Sodium :	call the new language with all the high-level goals "Tradeoff"
00:53:25	Zeeshan Lakhani:	Yeah, very far. I’d say rich polymorphism, intersections, resource types, refinement types, and such are still “early” days in everyday use.
00:54:05	Zeeshan Lakhani:	But a paper on verifying dist sys that’s good: https://drops.dagstuhl.de/opus/volltexte/2017/7126/pdf/LIPIcs-SNAPL-2017-19.pdf
00:55:18	Marc-Antoine Parent:	Thank you!
00:56:26	quinn:	https://www.hillelwayne.com/post/spec-composition/
00:56:38	quinn:	"WHY SPECIFICATIONS DON'T COMPOSE"
00:57:02	Marc-Antoine Parent:	Ha! Well, unsurprising
00:57:12	quinn:	(Obviously it's only a partial answer to a subset of the question)
00:59:59	Sodium :	asking datalog to count all the natural numbers >:)
01:00:28	Philipp Krüger:	Well, I've heard natural numbers are countable, so surely datalog will figure it out :P
01:00:51	Brooklyn Zelenka (@expede):	😆
01:01:51	Marc-Antoine Parent:	The compiler should detect and expand to +inf at compile time ;-)
01:03:17	aesakamar:	Re distributed memoization and reasoning about sideeffect free programs: Unison ❤️
01:05:05	Marc-Antoine Parent:	Is that not what Cambrian does?
01:05:30	Philipp Krüger:	Yeah, Quinn mentioned project cambria
01:05:37	Marc-Antoine Parent:	Missed it, thx
01:05:57	quinn:	Pieces of it! Cambria depends on a database of lenses + is much more imperative, but if we can keep things declarative we get lots of benefits (like what Brooke is saying now)
01:06:04	Philipp Krüger:	https://www.inkandswitch.com/cambria/
1 Like