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