Twisol

28 ms·

271.
by Twisol 4y ago
They make state machines leagues easier to reason about. Each state is its own function, and you tail-call to the next state (and pass along only the data it relies on, if you're doing things functionally).
272.
by Twisol 4y ago
These are two different problems, actually! The Byzantine Generals problem is concerned with arbitrary failure: a node may not simply fall offline, but may start sending garbage or otherwise act non-cooperatively. The Two Generals problem i
273.
by Twisol 4y ago
In 4, Bob only knows that he has stopped receiving messages. Alice may still be sending messages, but a mysterious fissure has appeared between their camps, and their couriers keep falling in.
274.
by Twisol 4y ago
It only takes one round-trip for both sides to be confident that the first message was received. However, the second party can't be sure the first party knows they received the message without hearing an ACK from the first party. As
275.
by Twisol 4y ago
Directed acyclic graph, yes.
276.
by Twisol 4y ago
I'm hopeful about this approach, honestly. We do build stateful flows in web applications, today, but we have to manually manage the serialization of that state to a shared store so that whichever worker the next request hits can pic
277.
by Twisol 4y ago
HYTRADBOI (the conference the OP was presented at) also had a talk on DatalogUI! https://www.hytradboi.com/2022/datalogui-rubbing-datalog-on-...
278.
by Twisol 4y ago
This talk blew my mind when I saw it "live". The lexical separation between client and server, within the same program description, reminded me a lot of Distributed Algol (see the chapter in Practical Foundations for Programming L
279.
by Twisol 4y ago
This is discussed in the article, where they used this fact to affirm that aphantastic individuals are indeed attempting to visualize (and failing), vs. simply not attempting. Moreover, they explain that in those who can visualize, pupils b
280.
by Twisol 4y ago
> When working on a large codebase or trying to plan out something like this -- you can't really go off of visual imagery. There's no "picture" of all the ways that various things in a codebase will interact, design d
281.
by Twisol 4y ago
"Normal forms" are definitely a thing, most clearly in linear algebra but certainly elsewhere as well. Being able to normalize any description of an object to a single unique canonical description is incredibly useful! But we don&
282.
by Twisol 5y ago
> Idempotence is usually used when talking about effectful code. Agreed! The idempotent operation acts on some state; how that state is modeled is an independent concern. > In other words, f(f(x)) = f(x). Which, as it just so happen
283.
by Twisol 5y ago
In your second example, if you run `send_message(id=1, body)` once and then run `send_message(id=1, body)` again, it behaves differently the second time than the first time, despite receiving the same input. So `send_message` is idempotent,
284.
by Twisol 5y ago
> A program is idempotent if when we run the program multiple times (on the same input), it will have the same effect as if we run it only once. Determinism/purity could be defined the same way; the difference hinges on your interpr
285.
by Twisol 5y ago
This only answers a small piece of your question, but it's important to realize that the mathematical notation you see is only how mathematics is recorded and communicated. Most of what goes into doing mathematics happens in your hea
286.
by Twisol 5y ago
> I got my first swe job this past August [...] I have now been on this team for 8 months, and I made 2 costly mistake back-to-back that is pushing back the release of a production feature by a while month at this point. > I was somet
287.
by Twisol 5y ago
Maybe is a sum because it was defined using sums. It's a monad because, from that definition, you can implement functions meeting the monad interface. "Monad" is more like an adjective than a noun. > I wonder if there is
288.
by Twisol 5y ago
For any type `a`, `Maybe a` is a type. We say "Maybe" in the same sense we say "List" -- it's obviously a list of some type `a`, but if what we're saying doesn't depend on any particular choice of `a`, the
289.
by Twisol 5y ago
Type patterns [1] are still unfortunately in preview (and have been since JDK 17), and record (destructuring) patterns [2] haven't even landed as a preview yet. I hope the latter get at least a preview in JDK 19 [3], but it looks like
290.
by Twisol 5y ago
As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensi
291.
by Twisol 5y ago
Yes, I don't especially disagree; I also think words are most useful when they mean something consistent and precise. Nonetheless, I think it's worth separating the merely terminological disagreement from the deeper semantic disag
292.
by Twisol 5y ago
I've finally found the article! It is "What do we want a foundation to do?", by Penelope Maddy. http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want... I need to reread it myself, but this
293.
by Twisol 5y ago
Yes, hence my desperate desire to relocate the article on what purposes a foundation may be put to. I say this as neutrally as possible, but I don't think "foundation" has such a singular meaning, and misattributing one &quot
294.
by Twisol 5y ago
I think Mike Shulman's side of the discussion in that thread is also very worth reading, and it's somewhat unfair to (perhaps unintentionally) characterize Lurie as the representative of mathematicians trying to talk sense into th
295.
by Twisol 5y ago
I've read rather too much of the fascinating comments thread you've indirectly linked to, but this nugget by Mike Shulman in that thread seems especially relevant to the present one: > If we distill it down from the categorical
296.
by Twisol 5y ago
The current development team didn't always build it, either. And the pressures and incentives are often biased away from improving things, no matter how much individual developers might want to. "You build it, you fix it" has
297.
by Twisol 5y ago
> This is a well written article, if long. That's Amos' brand, alright! ;) (<3 Amos)
298.
by Twisol 5y ago
A structure is a monad if you can nest one of itself inside another without a visible seam. If you have a binary tree whose leaves are also binary trees, is that meaningfully different from a single grafted binary tree? Not really. If you h
299.
by Twisol 5y ago
I've seen an internal Java-based web application (a digitization of some business processes involving what used to be paper forms) in which nested elements in a web page corresponded with subclasses in Java. Way high up in the hierarch
300.
by Twisol 5y ago
"To index" means to point, as with your index finger. An index, such as at the end of a book, serves to point into the main body of the work. In this context, I think of an index like a mass noun; the whole thing serves the purpos

More ›