The Verse Programming Language [pdf]

Can epic do that ?

Facebook a least "invented" a form a "passing time" (I'm being generous not to call it wasting time) that doubled as an advertising and marketing platform. And even that only took aff with the advent of smartphones, which enabled "using Facebook / twitter on the go" (and, more accurately, "on the loo").

When there's a VR helmet attached in every toilet, though... I'll sell hemoroid creams :)

(I'm pretty sure that's not what is discussed in these slides...)

- What's the advantage of introducing a new lambda calculus extension? What will we understand about Verse in virtue of the existence of VC that we don't understand about e.g. minikanren?

- How does the rewriting based execution compare with the search procedures of existing logic programming systems, and how does that impact how one would use Verse? For example, it sounds like they both want Verse to be purely declarative and performant enough to support the metaverse. But:

  - The way the slides expand out the choice of two variables makes it look like it's working in DFS order. The paper makes a big point of rewriting expanding out values "spatially" rather than in time. And I guess it's relatively clear how the rewriting system would produce DFS-like behavior ... but that's a problem isn't it?

  - E.g. minikanren as one of its key design points chose its interleaved search so that search could give comprehensive results on problems where DFS would (naively) never return, because it would go down some infinite rabbit hole. And minikanren, wanting to be more declarative, doesn't rely on "extra-relational" operators like "cut" which are important for prolog. This was supposed to have the impact that users don't need to worry about imperatively controlling the search, but this is only half-true in that users must pick the order in which variables are introduced extremely carefully.
  
  So if one says "x, y, z are all nats in (0, 1, ...) and x * x + y * y == z * z", it seems that, as with DFS, the rewrite system would include a path which tries to expand out and then check all of the (0, 0, z) possibilities to the left of any of all of the (0, 1, z) possibilities, etc. So even if under lenient evaluation there's _some_ tree that finds (3, 4, 5), and this may be reached in chronologically finite time, there's an infinite pile of work to be evaluated _to its left_. So can one never take the "first" element from this sequence, since it seems this means "left-most"? Or does this whole thing need to implicitly be restricted to searches over finite domains?

  It seems like either one must loosen assurances of ordering within sequences, or one must include "extra-logical" means to control the rewrite process.