you may or may not be aware that when he headed vpri, they did some substantial research into some of the other important ways to organize software, including things like array languages, david p. reed's work on spatially replicated computation, and cooperating communities of specialized solvers. in this talk, he also mentioned gelernter's tuple-space architecture, though you may have missed it. he definitely isn't arguing that oo should be the universal way to build everything, much less smalltalk; he's lamenting that no better paradigm than their research prototype has emerged since then
however, i do agree that there are some advances made since then that he doesn't fully appreciate, things like the importance of free-software licensing, roy fielding's work on architectural styles, recent advances in formal methods and functional programming, and the web's principle of least power
Bret Victor's DynamicLand seems to be a direct descendent of many of these ideas. RealTalk's reactive DB combines Linda tuplespace ideas with LISP 71 pattern matching and reactive semantics. Each Realtalk object is self contained and can't be 'messed with' externally. It's all introspective and reconfigurable, etc
Do you know anywhere where one can look into dynamicland more deeply? I've been interested in playing around with it for a while (hopefully I can get my hands on a projector lol) but have never found any details. Omar Rizwan's website had a cool post on geokit but that was all I managed to find.
I found out about this a few months ago through Cristobal's blog: https://cristobal.space/. Somehow didn't notice how the post mentions Omar's involvement at the top lol. Thanks anyway tho.
you'll probably have to talk to the dynamicland folks; i'm not sure what their current strategy is for getting it out into the world, but it doesn't seem to be the obvious 'upload the software to gitlab and hope for the best' approach
yes, agreed. you may or may not be aware that bret was a principal investigator at yc harc, along with vi hart, dan ingalls, john maloney, yoshiki ohshima (who posted this video), and alex warth, at least three of whom were at vpri. yc harc was sorta kinda headed by alan kay https://www.ycombinator.com/blog/harc
Yep, was definitely aware. It just seems like of all the projects at HARC, this is the only one that branched out from Alan's earlier ideas. The set of papers on https://worrydream.com/refs/ gives a good idea of some of the inspirations behind DL.
>you may or may not be aware that when he headed vpri, they did some substantial research into some of the other important ways to organize software, including things like array languages, david p. reed's work on spatially replicated computation, and cooperating communities of specialized solvers.
I'm very interested in knowing what array languages they were researching. The only thing I can find is Nile[1] but from the examples it doesn't look like an array language to me.
Pretty sure he would appreciate it for the guarantees those come with, but criticize them for being dead programs, that are not alive like for example the internet, one of his examples for systems, that started and from that moment on have not been taken offline to be changed.
This is really interesting; it’s really cool to think about the “statics” and “dynamics” of programming, and I while I have a basic understanding of functional programming (both the dynamic world of Scheme and the static world of languages like Standard ML and Haskell), I’m unfamiliar with these recent advances in functional programming and formal analysis. I’m wondering if you could share some links or references to some of this material?
i'm not the best person to ask, and i don't really know where to start
tla+ is getting uptake in industry, idris is sort of making dependent types practical, acl2 has more and more stuff in it, pvs is still around and still improving, adam chlipala keeps blogging cool stuff, so does hillel wayne, sel4 is an entire formally-proven-secure microkernel, you can try compcert on godbolt's compiler explorer, ləɐn has formalized significant mathematical definitions that working mathematicians use actively while metamath has an extremely convincing approach to proof and an ever-growing body of proofs of basic math, smt solvers like z3 are able to solve bigger and bigger problems and therefore able to tackle bigger subproblems of verifying software (and are easily apt installable and callable from python or from cprover's cbmc), cryptocurrency smart contracts have an incentive to be correct in a way that no previous software did (and people are applying at least idris to at least ethereum), ...
however, i do agree that there are some advances made since then that he doesn't fully appreciate, things like the importance of free-software licensing, roy fielding's work on architectural styles, recent advances in formal methods and functional programming, and the web's principle of least power