6 ms·
A Flexible Type System for Fearless Concurrency (2022) [pdf]
- TheRealPomax 3y agoThis needs [pdf] in the title.
- malf 3y agoI thought the days of “opening a pdf freezes IE for several seconds” were long past. What makes this painful for you?
- TheRealPomax 3y agoWho said anything about painful? HN posts that are direct downloads for pdf files are universally marked with [pdf]. Either because the poster remembered to do so, or because the title gets edited after the fact. This is not an article, it's a download, and should be marked as such.
- yencabulator 3y agoIt's only a download if your browser chooses not to display it. On Chrome, it's just another tab among tabs; you can choose to save to a file if you want.
- withinboredom 3y agoWhether or not to open on a mobile device? I usually don't open PDFs on a mobile because it is a pain to read.
- deleted 3y ago[deleted]
- deleted 3y ago[deleted]
- detrites 3y agoPDF's also present privacy and security risks (the question's old but answers been updated): https://security.stackexchange.com/questions/72037/what-are-the-security-risks-associated-with-pdf-files https://security.stackexchange.com/questions/72037/what-are-...
- quickthrower2 3y agoMany HTMLs have the same issue
- withinboredom 3y ago“Reading mode” usually solves this with HTML
- verdagon 3y agoTheir approach lines up pretty well with how we do regions in Vale. [0] Specifically, we consider the "spine" of a linked list to be its own private "region", separate from the elements' region. This lets us freeze the spine region, while keeping the elements region mutable. This mechanism is particularly promising because it likely means one can iterate over a collection with zero run-time overhead, without the normal restrictions of a more traditional Rust/Cyclone-like borrow checker. We'll know about this iterating benefit for sure when we finish part 3 (one-way isolation [1]); part 1 landed in the experimental branch only a couple weeks ago [2]. The main difference between the two approaches is that Vale doesn't assume that all elements are self-isolated fields, it allows references between elements and even references to the outside world. However, this does mean that Vale sometimes needs "region annotations", whereas the paper's system doesn't need any annotations at all, and that's a real benefit of their method. Other languages are experimenting with regions too, such as Forty2 [3] and Verona [4] though they're leaning more towards a garbage-collection-based approach, where Vale is more like a memory-safe C++. Pretty exciting time for languages! [0] https://verdagon.dev/blog/zero-cost-borrowing-regions-overview https://verdagon.dev/blog/zero-cost-borrowing-regions-overvi... [1] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3-one-way-isolation https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3... [2] https://verdagon.dev/blog/regions-prototype https://verdagon.dev/blog/regions-prototype [3] http://forty2.is/ http://forty2.is/ [4] https://github.com/microsoft/verona https://github.com/microsoft/verona
- tomas789 3y agoHonest question. Why many researchers in the area reach for a completely custom language? There is a huge barrier for new language. All the tooling, bindings for OS, tailor made libraries for specific use cases and so on. It all has to be done almost from scratch. Why not to start from what people already know and love and bolt your experiments on top of that? What I do with my DSL AmpLang is to start with Python, throw away parts I don’t like and add the things I’m interested in. It seems to work well enough and my language feels familiar for Python developers. I did not test that but many of existing Python programs would work out of the box in AmpLang. Python grammar is very simple. Even more so for 3.9 which does not have pattern matching.
- pjmlp 3y agoGreat piece of work. Where it kind of fails short, as usual, is when OS IPC, external resources or multiprocessing enters the picture, with the type system not being able to prevent external events from taking place. The concurrency remains fearless only for process private in-memory data accesses.
- dgb23 3y agoIn a broader sense, any type system can only guarantee internal consistency.
- pjmlp 3y agoQuite true, and often overlooked when discussing fearless anything in the age of distributed computing.
- eternalban 3y agoProtocols to the rescue, potentially.
- deofoo 3y agoI just love the beauty of type systems, the vast complexity and effort put into building an extensive architecture. And on the same time, systems without it are capable of wonderful things. Just beautiful.
- chombier 3y agoHere's the video of the talk: https://www.youtube.com/watch?v=yUtZwdGhxhw https://www.youtube.com/watch?v=yUtZwdGhxhw
- Sniffnoy 3y ago> Figure 2. Removing the final element of a singly linked list. Note that both the returned result and list remain mutable, and the returned result is no longer encapsulated by the linked list, unlike in prior work (e.g., [26, 46]). Note also that this function returns none on lists of size one, as it would be impossible to separate the list from its tail in this case. Huh, now that sounds like a substantial pitfall... any good way around this?
- deleted 3y ago[deleted]
- ObscureScience 3y agoUnless length of the list (a "Vector" in typical dependent type nomenclature) I can see the issue. I have not read the paper, but why is not a the empty list the value that returns None when called with this function? I assume the empty list is still a list in this type system?
- jmgrosen 3y agoNo, it’s not—-they’re passing in a “node”, not a list, which always contains both a head element and a (nullable) tail pointer. That’s why it can’t separate the head in the case of size one: the node must maintain a non-null head.
- lapcat 3y ago(2022)
- deleted 3y ago[deleted]