Some excerpts from recent Alan Kay emails
worrydream.com
worrydream.com
There's a YouTube talk by the author on the subject here:
The rough idea is this:
- creativity often arises by stumbling around in a problem space, or in operating "randomly" under an artificially-imposed constraint
- modern life is obsessed with metrics and goal-setting, and this has extended into creative pursuits including science, research, and business
- sometimes, short-term focus on the goal defeats the goal-given aims (see e.g. shareholder value focus)
- the authors point out that when they were researching artificial intelligence, they discovered that systems that focused too much on an explicitly-coded "objective" would end up producing lackluster results, but systems that did more "playful" exploration within a problem space produced more creative results
- using this backdrop, the authors suggest perhaps innovation is not driven by narrowly focused heroic effort and is instead driven by serendipitous discovery and playful creativity
I found the ideas compelling, as I do find Kay's description of the "art" behind research.
Reinertsen, in "Managing the Design Factory", describes the need for companies to generate high value information as efficiently as possible. Using Shannon's theory of information, he argues that low-information events are those events where the likelihood of either success or failure is high. Out of this comes the fact that you maximize the information output when the probability of failure is 50%.
How many of us take risks - professionally or personally - where the probability of failure is 50%?
I personally am not opposed if disclosed, since AFAIK (documented as of 2012 https://news.ycombinator.com/item?id=4156414) this gives access to other items purchased in the same time frame (whether the specific item is purchased or not) and analytics for links with no orders.
[1] https://www.amazon.com/Strategic-Intuition-Creative-Achievem...
A comment of mine from a year ago: "I think the way forward for AI will be in simulating human conciousness processes, including whatever limitations computationally that come with that. In this sense, I feel that the kind of AI that will break barriers first is going to be in a game, and not on a factory floor."
Though the book is slightly repetitive, what stuck with me is the idea of a "stepping stone approach". In order to discover something new or interesting, all we need to do is to find the next stepping stone to jump to. The rest is not is not in our hands. I tell this to myself whenever I think I have to have this "grand vision", which I never have so I don't do anything. I'm happy I stumbled upon it.
If you read the threads you'll see that he has frequently continued conversations long after the submission dropped off the HN front page, and many topics have gotten developed further than one usually sees. HN's archives are full of gold and for me this one of the more obvious veins of it.
If anyone wants to spend some time aggregating and collating these writings, as the OP has done from emails, I would see about getting YC to fund the effort, subject to Alan's permission of course. Email hn@ycombinator.com if you're interested.
I did a search in my mailbox and found a small branch of a huge discussion thread tree 555 days ago:
https://news.ycombinator.com/item?id=11958781
Perhaps we can build a "systemland" in some way.
Very important takeaway!
> Socrates didn't charge for "education" because when you are in business, the "customer starts to become right". Whereas in education, the customer is generally "not right". Marketeers are catering to what people want, educators are trying to deal with what they think people need (and this is often not at all what they want). Part of Montessori's genius was to realize early that children want to get fluent in their surrounding environs and culture, and this can be really powerful if one embeds what they need in the environs and culture.
This is so true on so many levels. Schools and university came to mind immediately. For me, the most striking fit is to educational articles and blog posts on the web.
When the www was young it was full of stuff that catered my intellectual curiosity. Nowadays content creation is driven by keyword research, search volume and CPC. After three paragraphs I usually know this will end in a call to action. Not that there wouldn't be any interesting stuff out there, but it is drowned in a sea of ever repeating trivialities.
What changed the most? How good I am at formulating a query? What kind of information I'm looking for? How good Google is at curating the first page? How much information is available? Sure hope its not that my queries are more trivial, or that my preferences for answers favors simpler,easier ones...
Thankfully I still get lost on Wikipedia (and Youtube), in a kind of what-is-all-this-I-need-to-know-more learning spree.
- we became impatient if not lazy - google does a huge job at parsing complex queries - the content is more organized in itself (html semantic markup, meaningful css classes, etc etc)
The other day I tried a tails/tor and .. i cant recall.. ipfs probably. This network is bare, so bare I felt excited just like the 56K days. It quickly went bad because there's a huge % of bad / crazy content, but still I felt entering a more interesting territory as a visitor.
I know what you mean, but should we be thankful? Learning is stimulating, but are we just indulging in it with little or negative results because we are acquiring misinformation?
Suspect part of it is also me and knowing how to phrase searches. Bit that just does not work to the same level on DDG.
In the 1970's a few dozen brilliant people could create a completely new and self-contained computer system because the entire computing world was tiny and fragmented. there wasn't the imperative to be compatible to all-pervasive standards (even IBM's dominance in business was being challenged by the minis).
These day if you want to create a new computer system that people will use you need at the minimum to provide a networking stack and a functional web browser, some emulation or compatibility system to support legacy software that people rely on, device drivers for a huge range of hardware, etc. All this not only takes a huge amount of work, it also punctures the design integrity of your system, making it into a huge mountain of compatibility hacks before you even start on your own new concepts. But the deadliest enemy of innovation is the mental inertia of masses of users with a long history of interacting with computers. They are no longer the blank slates who have never seen a computer you had in the 70's.
Even in the realm of art people realized that the romantic or modernistic model of artistic revolution that Kay invokes is untenable and retreated into postmodernism.
One possible approach that doesn't require writing a full compatibility layer is virtualization. Run your new system alongside a mature system like Linux, then rig it up so windows can appear inside whatever new environment you come up with. You do still need to write the code to send events and get pixel buffers, but it seems like much less work overall.
I don't know an alternative except to do everything new within one window, which would be at least as bad.
http://blog.ycombinator.com/harc/
https://news.ycombinator.com/item?id=11679680
In September "eleVR" said it was leaving YC research:
http://elevr.com/elevr-leaving-ycr/
I presume these e-mail excerpts are inspired by the end of HARC too? What happened?
In the thread about first year reports a couple months ago, someone suspects that funding has ended too. Also, Bret Victor's work and name are conspicuously missing from the first year reports.
How long do they commit to funding for? How do they evaluate when to continue funding? What do they consider "success"?
A year and change is incredibly short for basic research. If at the outset you only planned for a year of funding, then you can't expect any results. It's almost wasted money. So I think that something happened to make them discontinue the funding.
> The misleading thing about Linux is that it IS IN FACT a big idea -- it's just not a technological idea. We already knew how to write monolithic kernels. But the real innovation is the software development process. The fact that thousands of programmers can ship a working kernel with little coordination is amazing. That Linus wrote git is not an accident; he's an expert in software collaboration and evolution.
https://news.ycombinator.com/item?id=15164092
From your comment, I think the funding and development process of these post Bell Lab/PARC research projects might need a paradigm change from technology idea oriented to social development oriented due to the reality of our highly networked social environment (the dream of Licklider).
If we read the CRAZY eleVR thread as a tree/forest, https://news.ycombinator.com/item?id=15162957
We can see that how much misunderstanding of each other exists in our tech community. There are much deeper social development problems to be solved than simple VC or philanthropy funding.
@vihart was right saying
> HN. You're a weird place.
It is a more fundamental problem that vihart and gang can’t solve. And that would be an opportunity at another meta level.
Think what Lick would do.
You have a point that, ironically, the success of Licklider's vision may have changed the nature of collaboration for the worse in some ways. It's been a huge net positive, in that humanity as a whole is more productive, but there are things that have been lost.
(Or maybe another way to look at it is that Licklider/Engelbart's vision has been watered down, and you could solve these communication problems with better software design.)
Another example I recall is that Rob Pike said that Bell Labs was a wonderful environment because everyone had to physically sit in the same room, huddled around big shared computers. There is a natural exchange of ideas in that environment, which leads to big research breakthroughs. When Ethernet and personal workstations came around, suddenly you could sit at your desk and close the door and put your headphones on.
I personally noticed that irony at my own job. Often people would be talking more to people in a remote office than the person sitting next to them. And sometimes people would chat electronically with someone in their own office -- e.g. if they didn't want to take off your headphones or disturb other officemates!
I also wonder what a new model for funding basic research looks like. It seems like YCombinator would be a logical entity to fund such research, but as far as I can tell, it was a failed experiment.
And I think there is some danger in longing for the "golden age". I was reminded in reading the "Dream Machine" that a lot of it was driven by fear of the Soviets (Sputnik, etc.). And I also wonder if what made it work back then is no longer present, for better or worse.
On the other hand, on top of the computer hardware/software communication layers where this conversation takes place, there is a profound layer that we seem to take for granted and not consciously aware of (like fish in the water), i.e., written language composed and consumed by real human being (English in this case). To communicate effectively with this distributed (non-local in space) and asynchronous (non-local in time) layer, we need more contexts other than the words themselves. In Rob Pike's Bell Labs and Alan Kay's bean-bag-chaired PARC, local synchronous face-to-face communication would be much more effective because the audience were from the same background and shared the same context.
Let's take a look at the contexts of Bret Victor's blog post "Some excerpts from recent Alan Kay emails". These are excerpts of private written communication (emails) between Alan Kay and Bret Victor. We could imagine what Alan had in mind when he wrote those emails, or what Bret had in mind when he read them, further more, why Bret made those excerpts and posted them on his blog. However, since we were neither Bret nor Alan, we can only read them within the constraint of our own contexts. We can only guess what message Bret wanted to send with his blog and we are not even sure we (HN community) are his intended audience.
I am sure there are some YC funders reading this and the fact that we don't see any of them making a statement here shows that they are also under the constraint of their contexts. So I guess the challenges and solutions to funding of research lie upon these contexts as well.
It is all about pink and blue planes.
i am going through licklider's 'the dream machine' book. it is quite long, and dense but ties together lots of individual threads (for me at least) that were kind of floating loose otherwise. i had known about luminaries in the field (and their work) specifically, licklider, shannon, norbert-weiner, cerf and kahn, metcalfe, von neumann, vannaver bush (to name a few) but this book brings them together.
interestingly though, licklider's background was in psychology, as opposed to ee/maths. did we lose some of the diversity of perspective ?
another book, that i found to be pretty good is 'the idea factory', it complements the 'dream machine' book quite well.
edit-001 : fmt changes, and added reference to another book.
[0] http://www.squeakland.org/resources/books/readingList.jsp
The answer to this question is almost right in the emails: the focus of funding research switched from visionary work of defining problem space to exploration of solution space. Engineers are people who are educated, perhaps sometimes predisposed, to solve problems, not find problems worth solving.
https://lobste.rs/s/i9s39q/best_books_you_have_read_2017#c_z...
It looks like you made at least four of the same points that I did.
That's a vision that recognizes the value in creating tools, not constrained solutions for the current problem. Freedom can be frightening[1], but letting people explore what is possible with your new tool sometimes leads to unexpected uses and the occasional paradigm-shifting discovery.
[1] (with apologies to DHH[2]) If we give people unconstrained tools, they might change the String class to shoot out fireworks at inappropriate time!
I'm sure there's a cultural effect here as well. Seems like there are fewer large companies that are willing to just let technologists "muck around for a bit" swinging for the fences without some kind of goal.
But, I just wonder, if VC-funded startups are where new tech grows, we end up just focusing on incremental improvements, instead of potential large leaps.
I wonder if this is true. Many of the major computer industry companies have labs: Google, Microsoft, IBM ... (Apple? Facebook? Amazon?)
I wonder if it's more or less than before.
Because I feel like I've read a few of these posts, watched similar talks, and I nod along and agree every time. Only problem is, I'm not a wealthy benefactor, director of a research institute, or a business exec with control of discretionary R&D funding.
Where do those people hang out, what would convince them like this post convinces me, and is anyone working on that?
I think it is working in research (given for example that some of the papers in conferences like POPL are just great). Of course you won't hear from those instances where it is not working (until it does).
The problem is you somehow have to decide who to give money to, and you cannot possibly know who carries a vision inside of them that they are actually able to realise given enough funding and time.
-- I have seen these types of situations so many times while project implementation.
Unless there are any great results, no, they are not.
Tons of research money where poured into AI in the 60s-70s too, and when it got nowhere great, it all folded in the so-called "AI winter".
Billions poured into AI have produced some interesting tricks but little that changed the entire world of computing in the way those things have.
Yes, billions have been poured into AI and we still have no strong AI. That just shows that it's a problem that is way more complicated that inventing the concept of a pointing device, making computers talk to each other, or having applications show something on a screen that isn't text. The people in the 80s weren't smarter (or dumber) than the people of today, there were just a lot of low hanging fruits back then.
Even if this were true, which I disagree with, it has changed the world. Just because we don't still use the iPod anymore doesn't make it any less brilliant.
> The people in the 80s weren't smarter (or dumber) than the people of today, there were just a lot of low hanging fruits back then.
They didn't just take the low hanging fruit. In the 60s it was assumed that computers would just get bigger and bigger. They had to take the highest hanging fruit that everyone thought was ridiculous. They had to envision an entirely different world. So perhaps they weren't more intelligent but they had a more powerful vision of the future.
You're probably laughing at similar people today.
The people being given money for AI are expected to work on AI, not on whatever they think is cool.
Hire a bunch of smart people, give them advance funding for 5 years without strings attached, tell them to build the future without specifying what that means.
From a personal view I have plenty of ideas for things never built before, but I lack the time and energy to do it after hours and I can almost never fit it into the scope of my professional work. Sometimes this makes me sad.
Parc was "effectively non-profit" because there was no way to collect or monetize reams of user data like there is today. If there had been, either Kay wouldn't have gotten that agreement or Parc would have been much more selective about what constituted "results."
For example: how many companies have solved the talk-to-our-computers-and-our-computers-talk-back problem now?
Xerox was at the time the world leader in handling literal reams.
A huge portion of data processing was related to managing customer data, mailing lists, etc.
Someone can correct me if I'm wrong, but I've never seen anything Kay wrote from the 70s or 80s that discussed the implications of mining user data on such an enormous and regular basis as is currently done. And I doubt Xerox itself thought of that category of user data as being valuable outside of research, or in any way significant the way "customer data, mailing lists, etc." were. But today, that user data is assumed to be valuable and can cheaply be collected and monetized. So even if some Parc-like team exists today, the results will be practically locked-down to keep a competitive advantage over others. Or it will make much smaller strides with specific goals in mind-- like Mozilla with Rust. Or it will clone and improve upon existing proprietary technology and make it available to the public-- like GNU.
It's a bit like reading someone wax nostalgic about Bitcoin's initial bootstrapping mechanism and complaining that today's altcoins don't put enough emphasis on distributing the tokens to people who aren't speculators. That's fine as a description of a problem, but its a fairly toothless observation in terms of solving the problem. Distributing tokens when nearly nobody is watching is a completely different problem from distributing them when everyone is not only watching but also speculating. Similarly, having a research team do work that is a pubic good when nobody thinks the data generated is something that can be directly monetized is a completely different problem from trying to do the same when the greater part of the economy depends on everybody watching, collecting, and monetizing the data that your software/hardware generates.
"An important part of any art is for the artists to escape the "part of the present that is the past", and for most artists, this is delicate because the present is so everywhere and loud and interruptive. For individual contributors, a good ploy is to disappear for a while"
reminded me of John Carmack explaining in his .plans how he would go off and seclude himself for a couple of weeks to start a new iteration of the id technology.
I also totally get the point of funding problem finding versus funding business plans that are full of bullshit and pretend to have a risk free solution with a play book that just needs some money to execute it linearly step-by-step. So, for that part it is written very well and the point is clear.
Another topic is: would all kind of innovations really emerge if the funding mechanism was radically different in the last 20 years? Would we see all kinds of big leaps or was ARPA-Parc just a serendipity moment that couldn't be repeated no matter what the funding structure was?
On two occasions I've had VC types (in one case post-beer) tell me they almost never fund anyone who doesn't have (paraphrasing) "presence" or "a reality distortion field" etc. I would have assumed it to be subconscious but these comments convinced me that it's a conscious explicit bias in at least some cases.
This is a really outstanding book on the topic:
https://en.wikipedia.org/wiki/Quiet:_The_Power_of_Introverts...
Put enough weaponized extroversion and alpha primate signaling behind it and you can get people to invest in millions in absolute BS. You can also over-inflate the value of something real to stratospheric degrees. See also: Uber.
On the other hand if you have an underspoken introvert try to sell something outstanding, the majority of businesspeople will not pay attention.
I have seen a case where a meek soft-spoken woman tried to pitch a mobile startup with outstanding user base growth, revenue, and cash efficiency numbers and got yawns. She wasn't asking for much. This was seed stage stuff and these were crazy amazing numbers. In the same pitch fest the investor panel perked up for a number of vapid pre-revenue proposals backed by more extroverted alpha personalities. I don't think it was just sexism since one of these was also a woman. (I suspect some sexism is actually this bias since it may be tougher for women to play the alpha primate card with men.)
Most innovators ("artists") are more on the introvert end of the spectrum.
Edit: this may be rational for funding things that rely heavily on in-person salesmanship, but it's applied broadly.
Edit #2: another reason this may be rational for VCs is that they are only thinking about their cash-out. They may be looking for people who can pump the value of the company's stock to later investors more than people who can actually deliver lasting value. The company's product is its stock, not its product.
(1) Breakthrough technologies and/or amazing numbers.
(2) Introverted founders passed over by other investors.
(3) A sales process that is not in-person where being introverted, understated, or shy is not a major handicap. Companies with mostly inbound, viral, indirect, or automated sales processes or that can outsource sales easily would work.
What tools could you use to decrease the friction caused because introversion makes a founder harder to find?
I believe that for workstation/desktop computing we have already hit stagnation. I also suspect that programming languages have not advanced in any significant way since around 1990. By this perhaps surprising claim, I mean that the languages available today are no more capable than those available in the 1980s.
I would have said not much since 1970? 1950? What big new things have their been?
While there certainly are amazing people doing amazing things that deserve recognition, it seems increasingly clear to me that if any of them weren't there, the space would have been filled, and quickly. Maybe in different ways and things wouldn't be the same, but history is so full of independent near-simultaneous invention of practically the same things that it seems that a lot of ideas end up being realized not because of some unique intellect, but because their time has come, and the best these people can do is speed it up a bit.
Marketing and adoption is a different issue - I think William Gibson got it right: "The future is already here – it's just not evenly distributed."
A lot of the challenge of innovation is not the innovation itself, but getting the knowledge to filter out there. Arguably, it's first the last decade or so that languages like Lisp and Smalltalk has won people over - not by themselves, but by the success of an increasing array of languages created by people who were inspired by them that themselves have taken years to get traction.
And even then there are so many low hanging fruit that has not seen traction because, frankly, people are busy, and the amazing stuff often isn't the work most likely to pay the bills then and there.
People are often hostile to things they don't know. Not taking this into account when trying to introduce new things is a recipe for disaster.
This means ...
– picking up developers from where they are, not telling potential adopters "if you write Java-like Scala we don't want you here".
– meaningful documentation, not answering efforts to improve documentation with "it's not necessary, because everyone already knows Scala".
– describing and explaining design choices like companion objects, type classes, context bounds, and so on; not expecting that beginners will understand their superiority through osmosis.
– making technologies accessible to people on their platforms, not treating backends such as Scala.js, Scala on Android or Scala-Native as add-ons for existing Scala users (or worse).
– taking tooling seriously, and not releasing major versions of the language without tooling support. Or breaking compatibility in minor versions like in Scala 2.12.
– clean-ups that removes unnecessary baggage from the language and its libraries. Not lecturing people about the number of keywords or counting the lines in the language's grammar in comparison to other languages.
Haskell does some things better in this regard, but both are far from a convincing value proposition over "worse is better" approaches like Kotlin (which will probably swipe the floor with Scala in the future, because they address the bad parts of Scala).
> What we need is “a formal semantics for a language, with practical proof principles for designing correct programs”.
However, I'm not disappointed in industry languages, because I don't actually expect anything from them.
(0) Haskell and Scala are already very complicated, and they are becoming even more complicated at a very fast rate. This will only make life harder when we finally bite the bullet and admit that we need a formal semantics for the mess we have created.
(1) Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means.
(2) On more philosophical grounds, the extended community behind typed functional languages draws inspiration from the wrong source. Martin-Löf type theory is doubtlessly a beautiful foundation for mathematics, but it has a fatal flaw for programming purposes: it makes no distinction between values (which are already there, you just use them) and computations (which you need to run to produce values, and might have effects during the process). As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound.
(3) There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages. Alas, type theory is conspicuously silent about FFIs. Is this perhaps because of a refusal to acknowledge that computation is a prior notion, which types can help organize, but by no means define?
It's very hard to know what we need formal semantics for if we don't simultaneously try to write practical programs. There's a tick-tock pattern at work here: start with a clean formal language, figure out what extensions are needed to write practical programs in it, at first in an ad-hoc way, then figure out a way to make that extension in a sound, compatible way, then finally form a new clean formal language that accommodates these extensions. If you just want a language with formal semantics, ML or Haskell 98 exist already; Scala or GHC Haskell extend these to languages we can write industrial programs with, and then Dotty or Idris are clean formalisable designs with the lessons learned from this.
> Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means.
Not my experience. I've found HKT and dependent types extremely useful in practice; they give me a simple way to directly encode the business properties I care about verifying. Of course if you've come up with something useful I'm interested, and I'm sure many others would be, but I'd strongly disagree with the notion that what the academics are doing isn't useful.
> As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound.
Not at all convinced that e.g. Idris-style totality is "unacceptable". What's the problem with it?
> There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages.
Again not at all convinced. Certainly my practical Scala experience is that it's good for everything.
This is not possible, and the history of Haskell, Scala, and to a lesser extent OCaml, is precisely the evidence for it.
> Not my experience. I've found HKT and dependent types extremely useful in practice;
In practice, most uses of HKTs or even term-level HOFs are just bad workarounds for
(0) The lack of a proper hierarchical module system, allowing type components to be shared by fibration.
(1) The lack of properly designed data structure libraries with decoupled concerns. For example, you need traversals and folds to manipulate sets and maps, but you don't need them to manipulate search trees (i.e., trees that allow you to do binary search, rather than ADTs that might use binary search under the covers).
> they give me a simple way to directly encode the business properties I care about verifying.
Do you actually verify them? How exactly do you verify Scala programs in the absence of a formal semantics for Scala?
> Not at all convinced that e.g. Idris-style totality is "unacceptable". What's the problem with it?
“There is no largest class of recognizably terminating programs.”
https://mail.haskell.org/pipermail/haskell-cafe/2003-May/004...
> Certainly my practical Scala experience is that it's good for everything.
One thing that I find useful, due to my current job, is numerical linear algebra without array bounds checks at runtime. Have fun doing this in Scala.
Then how do you explain the existence of e.g. Idris or Dotty?
> In practice, most uses of HKTs or even term-level HOFs are just bad workarounds for
> (0) The lack of a proper hierarchical module system, allowing type components to be shared by fibration.
They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want. Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry?
> Do you actually verify them? How exactly do you verify Scala programs in the absence of a formal semantics for Scala?
Any verification method has a false-negative rate. I use a combination of trusting the compiler's typechecking, sticking to the scalazzi safe subset and enforcing with linters etc., manual review of recursion (limiting the cases where it occurs as far as possible) and fast and loose reasoning.
Maybe I'm missing something, because there always seems to be some disconnect in these conversations: as far as I can see any method that lets you associate logical deductions to your program and mechanically verify that those deductions are legitimate is verification, and I can certainly do that with propositions-as-types in the Scala type system. I don't verify the faithfulness of the compiled code, but many verification systems don't do that either. I don't have a proof of soundness, but plenty of verification systems don't have that.
> “There is no largest class of recognizably terminating programs.”
Sure. But not all recognisably terminating programs are important or useful. To form a terminating language we have to have a finite limit on how many levels of nested 'eval' we can do at compile time, sure (though I see no reason we can't form a parameterized family of languages and pass the "depth" as a compiler argument). That's irritating, but it's a big jump to "unacceptable"
> One thing that I find useful, due to my current job, is numerical linear algebra without array bounds checks at runtime. Have fun doing this in Scala.
"Without array bounds checks at runtime" is not a real requirement. The real requirement would be something like "using x amount of CPU" or, ultimately, "at cost of no more than $y". FWIW I did numerical linear algebra in Scala in production at a previous job; the benefits outweighed the costs.
More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language. Yes the current implementation doesn't do it, but that's a contingent fact about the current implementation, not something fundamental.
Have fun convincing people to port their existing Haskell and Scala programs to Idris and Dotty, respectively. In particular, Idris is not even remotely similar to Haskell beyond the syntax - it even uses a different evaluation strategy!
> They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want.
The trouble with Haskell and Scala-like higher-kinded type constructors is that they are merely parameterized by other type constructors, rather than by entire structures. (It is as if, in mathematics, all functors were functors from Set!) Haskell and Scala attempt to remedy this situation using type classes, i.e., identifying every type constructor `T` with a canonical structure whose carrier is `T`. But, what if you need to use two different algebraic structures, both having `T` as their carrier? For example, say you need to use maps whose keys are lexicographically ordered strings, as well as maps whose keys are colexicographically ordered strings. Do you create a `newtype` wrapper as in Haskell? Or do you use different implicits in different contexts, and risk conflating maps created in one context with maps created in the other?
This problem doesn't exist in ML, because functors allow you to parameterize entire structures by other entire structures, not just their carriers.
> Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry?
What do I know. Ask the industry, not me.
> I use a combination of trusting the compiler's typechecking,
Trust is neither here nor there. Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you.
> sticking to the scalazzi safe subset and enforcing with linters etc., manual review of recursion (limiting the cases where it occurs as far as possible) and fast and loose reasoning.
That's a perfectly fine set of software development practices, but it's not verification.
> I don't have a proof of soundness, but plenty of verification systems don't have that.
Then all you have is a fancy linter.
> More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language.
Um, the inability to statically verify array index manipulation using Scala's type system?
> "Without array bounds checks at runtime" is not a real requirement.
Not paying the runtime cost of superfluous runtime checks is absolutely a real requirement in my current job.
> More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language.
It can't be implemented as an ordinary library in the existing Scala language without relying on unsafe features (e.g., a C FFI). Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials.
> Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you.
What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". Or perhaps it would be better expressed via elimination - "if I provide eliminators for all my constructors for type A then I can eliminate any expression of type A". I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no?
> Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials.
What is it that we can't do currently? I mean, I can define a natural number type, I can convert between values and types in both directions. I can't use ad-hoc polymorphism with a type defined at runtime (the types I form at runtime must be phantom) but I wouldn't expect to do that in well-behaved code in the first place? The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. What am I missing?
This is probably sufficient for a Coq-style proof assistant, but from a general-purpose programming language I expect more. See below.
> I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no?
A type system can and should guarantee that you can't create values of a (positive) type other than by using the type's introuction forms.
> What is it that we can't do currently?
(0) The obvious: Be sure your program won't attempt to read from or write to a close file.
(1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking.
(2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking.
etc. etc. etc.
> The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala.
Are those casts safe without runtime checks?
---
In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs.
I can do that in Scala with monadic regions, which only need existentials/rank-2 types.
> (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. > (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking.
I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix.
I'm not saying any of this is as easy as it should be, I'm asking how "real" dependent types would be different from what Scala currently has.
> Are those casts safe without runtime checks?
No, we'd make the runtime check at the point of casting. What I mean is: the only way something I'd want to type as an array of length n could ever get into my program is (ultimately, once we flatten out all the arithmetic from e.g. concatenating arrays of length p and q), either a literal array of length n, or a manually checked cast of a dynamic-length array received at runtime.
> In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs.
My experience has been that types are more than good enough. My defect rate is much, much lower than it needs to be, lower than I can really justify putting any more work into, and I don't feel like I'm close to the limits of what's possible with types.
Monadic regions are inflexible. As I have previously told you on lobste.rs, try implementing braided allocations:
(0) Allocate A
(1) Allocate B, do something with A and B together, deallocate A
(2) Allocate C, do something with B and C together, deallocate B
(3) etc.
Turns out, you can't, because monadic regions are strictly LIFO. Lest you think this is just a theoretical exercise, this allocation pattern is used in the implementation of concurrent database indices.
> I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix.
The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list). To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous.
> No, we'd make the runtime check at the point of casting.
Then it's effectively dynamically typed, don't you think?
> My experience has been that types are more than good enough.
Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up.
> My defect rate is much, much lower than it needs to be
Lucky you. Mine has to be zero, but it's always positive, sadly.
Earlier in this thread you said "this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's" - aren't monadic regions exactly a case of wrangling more verification out of a relatively simple type system rather than building something more complex?
There will always be things we don't know how to do; monadic regions themselves seemed impossible until they were implemented. I don't think we've put anywhere near enough effort in yet to conclude that it's impossible to extend that kind of approach to support braided allocations; indeed that's the sort of thing I'd expect the academic process you deride to come up with.
> The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list).
The Scala type system can implement Turing-complete computation, you can do arithmetic with type-level numbers, so I don't see that the array design would needs to anticipate anything? Accessing a specific element could demand evidence that that element was within the array's bounds, operations that form new arrays would need to provide evidence about that array's bounds. But the user is free to connect those two ends together in arbitrary ways.
> To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous.
Um, I do say this. In a language that has first-class functions etc. I don't need any language-level support for sum types (e.g. pattern matching); Either#fold covers all the same use case. Language support is a nice syntactic convenience but nothing more than that AFAICS.
> Then it's effectively dynamically typed, don't you think?
No, because the type system is still checking that my deductions are valid, that my conclusions follow from my premises (e.g. if I concatenate an array that I've dynamically checked to be of size n with one that I've dynamically checked to be of size m, I statically know that the result is of size n + m). I'm just adopting an extra premise of "this particular runtime size check is correctly implemented"; of course if I adopt a false premise then I'll deduce nonsense, but that's on me. I don't see any qualitative difference between having the (outside array of unknown size -> array typed as being of a given size) function be part of the system versus implemented by me.
> Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up.
I don't prove everything, but I feel like I could; since I'm going to be using types anyway, I don't feel the need to pursue non-type ways of proving things unless and until I hit something that I want to prove that's harder to prove with types than it should be, that feels like an easier way to prove it should exist. So far I haven't.
Substructural types are a much, much, simpler addition to a type system than rank-N types, rest assured. For instance, substructural types don't impede global type inference. In fact, adding substructural types to HM require minimal changes to how the type checker works. Read ATTaPL, chapter 1!
> The Scala type system can implement Turing-complete computation, you can do arithmetic with type-level numbers, so I don't see that the array design would needs to anticipate anything?
By itself, a Turing-complete type system does not give you the ability to enforce arbitrary program properties. It only guarantees that you can wait arbitrarily long for the type checker to complete. Kind of impressive, but not useful.
> Um, I do say this. In a language that has first-class functions[sic] etc. I don't need any language-level support for sum types (e.g. pattern matching); Either#fold covers all the same use case. Language support is a nice syntactic convenience but nothing more than that AFAICS.
Encoding data as particular higher-order procedures only works in an effect-free language. (Nontermination counts as an effect!) Mmm, like Scala:
trait ChurchBool {
def pick[A](x: A, y: A): A
}
object ChurchTrue extends ChurchBool {
def pick[A](x: A, y: A) = x
}
object ChurchFalse extends ChurchBool {
def pick[A](x: A, y: A) = y
}
object ChurchWTF extends ChurchBool {
def pick[A](x: A, y: A) = pick(x, y)
}
> I don't see any qualitative difference between having the (outside array of unknown size -> array typed as being of a given size) function be part of the system versus implemented by me.
Here is an important qualitative difference: A runtime check that checks something that is statically knowable introduces an unreachable control flow path.
> I don't prove everything, but I feel like I could
Whereas I actually prove everything, and in the process have found a practical boundary between what (IMO) is reasonable to prove with types, and what I'd rather prove using other technology.
Scala pervasively allows nontermination, sure. All the program properties I have are up to "if it terminates ...". (I mean, I would claim I work in a fragment of Scala that disallows definitions like ChurchWTF#pick, but I can't really justify that without formalising it). Language-level support for sum types doesn't change that; programs written in Scala carry just as much risk of nontermination as programs written in Scala-without-pattern-matches.
> Here is an important qualitative difference: A runtime check that checks something that is statically knowable introduces an unreachable control flow path.
I'm not talking about having runtime checks for things that are statically knowable, I'm talking about runtime checks for things that aren't statically knowable like the size of an array received from an external source. Again, how is that any different from what you would do in a language with "true" dependent types?
Admitting nonterminating computations is actually a good thing. What's a bad thing is conflating computations with the values they produce. In other words, the types `Bool` and `ChurchBool` are not isomorphic.
> I'm not talking about having runtime checks for things that are statically knowable, I'm talking about runtime checks for things that aren't statically knowable like the size of an array received from an external source. Again, how is that any different from what you would do in a language with "true" dependent types?
There's no difference here. But you totally glossed over my point that your abstract type of arrays with a member type of indices would have to be bloated with every operation imaginable on indices.
Well, for a sufficiently low defect rate, I suspect it would take an order of magnitude longer (for normal developers) to achieve it in C, Smalltalk, or most Lisps. Ada perhaps not, but then maybe it would've taken the order of magnitude longer to implement, particularly if you factor in making enough money to buy the development tools first. Then as now, the future is not evenly distributed.
I mean, you're undeniably right on one level: for a small, standalone executable whose main task is bit-banging, where a high defect rate is acceptable, it was possible to bash that out 20 years ago at a similar speed to what you can do in today's languages. But I think that's actually a much smaller niche than it first appears, and not where the focus of our efforts has been because that's not actually what businesses most need.
> What we do benefit from is the availability of libraries, IDE's, and various frameworks. These, I would argue, rather than innate abilities of the modern languages are what enable us to be more productive (assuming that we are).
I think the ability to write long-term-maintainable, general-purpose libraries or frameworks is actually very tightly tied to the languages we use.
Nope. Not even close. We haven’t even made a user-friendly function editing tool. After that happens there will be another Cambrian explosion on the desktop.
Let me see if I can list more things like that...
Well, smart contracts. Those have approximately zero adoption and will probably constitute a double digit share of scripts in the future. We don’t even know how to write them yet. You won’t be writing smart contracts by talking to Alexa... not at first anyway.
What else... I think if I can come up with three I will have proven my point...
Well, a shared spatial computing environment. VR will encourage prototyping of libraries for structuring that stuff. But there’s nothing about shared computational space that necessitates a headset. I think most of what VR will do is show us new ways to structure desktop software.
And those are just things I, a person from the 80s, can point to and say “we haven’t figured this out on the desktop yet but we will”. That’s not even admitting the things we can’t even imagine.
I would say we have designed less than 1% of the computational structures that will come standard on a mobile phone in 2050.
We’ve been advances in for decades—approaching human lifespan timescales—so it sometimes feels like we’re close to the end. But we’re just at the very beginning of discovering the final form of “windows”.
That's not a problem I see, because this is not about Alan Kay's personal track record.
The kind of organizational freedom he describes was available in Park and Bell Labs, and it wasn't just Kay, but tens of people, one after another creating the most important technologies, while it was on.
First, that's not what appeal to authority means. It doesn't mean, "Don't be interested in what Einstein thought," for example.
Second, ironically, the big problem in our industry is that no one ever listens to those who have gone before. It's Alan Kay, not Alan Key.
We reinvent technology, package it with a new logo, give it a new name, and run into the same problems as before, until someone comes up with a new technology to replace it, which is the same technology again, ad infinitum.
You really need to listen to authority, because, frankly your software sucks. How do I know? Because all software sucks. Alan Kay, not Key, is one of the few people who understand that and understand what kind of creativity might lead us out of this mess. We should all be interested in what he's saying.
> I once gave a talk to Disney executives about "new ways to kill the geese that lay the golden eggs". For example, set up deadlines and quotas for the eggs. Make the geese into managers. Make the geese go to meetings to justify their diet and day to day processes. (etc.)
however it's really hard to argue that Apple, Microsoft, or indeed IBM or Disney ever killed the geese that lay the golden eggs.
Or if they did, they had plenty others running around.
In this context, you're not talking about the geese, but about the eggs. For example, for Apple, one such golden egg is the iPhone, and what Kay talks about is how there are many capable people to turn this golden egg (invention) into coins or platinum (product => shareholder value).
But the geese are not the products; the geese are the inventors. Jobs turned the failing Apple around from outside its own context. Microsoft missed out on the entire phone eco-system. Lots of people would attribute these long-term business fails to exactly what Kay talks about here.
Which makes more sense. It's hard to kill successful projects, but incredibly easy to build an atmosphere where creative people and new ideas are not welcome.
Just right.
UBI has a lot wrong with it, but I'll just start and end with a first principle: Taxation is theft and therefore, government and UBI are immoral.
I advocate for freedom and consent, especially as it pertains to economics. The income I earn through producing goods and services that I exchange voluntarily with other individuals should be mine to keep; all of it. Anything less is not freedom and certainly not consent.
Taxation drives the economy. By creating demand for money. No taxes, no economy.
If not for taxation, who will pay for the police that keep you safe, the education programs that likely educated you (assuming you had some publicly funded education) and most of your customers, employees, and business partners? Public health that prevents epidemics? The list goes on forever.
Maybe everyone should have those opportunities. Maybe that’s the future. Maybe it’s the bright side of the consolidation of wealth that’s only accelerating.
For details checkout geo-libertarianism. But in short the argument is that the common resources, “land”, should be allocated according to the preferences of the commons (see John Locke), not the individual. In practice have land owners pay the would be non-owners it’s full market value for the privilege of being called the owner (see Rawls, Justice as Fairness for this step). Call it a land value tax (see Henry George) or call it land rent. However, since it’s a payment to the commons, not the state, the only thing to do is to divide it fairly as a public dividend.
End result: a fair and proper UBI.
Can someone explain to me why this comment is deemed to be irrelevant?