Gradual Programming
willcrichton.net
willcrichton.net
> A basic observation about the human programming process is
> that it is incremental. No one writes the entirety of their
> program in a single go, clicks compile + publish, and never
> looks at the code again. Programming is a long slog of
> trial and error, where the length of the trial and the
> severity of the error depend heavily on the domain and the
> tooling.
If you wanted to change the world of programming I would think of a way to abstractly describe dataflows in the vain of unix pipes. Define every part of the transforms you need to do on incoming data, where those responsibilities should be, and then link them together. Current abstraction methods are subpar: they require inherent complexity, are language specific, and are not easy to change after you've using them (unless you have adapters on every part of the code base which in it's own right becomes a mess).
Discovering as you go is totally fine, and dominates what I write. It's also very nearly your only option when learning something new. Sitting on millions of lines of code, integrating with dozens of other systems... you often simply don't know what you need to do up-front, so you iterate and explore until you do. Gradually tightening the constraints of the system fits this kind of thing perfectly and I love when it's easy to achieve. It gets you both a faster start and a safer finish.
In contrast, entirely agreed - I've written a few low-kLOC projects start-to-finish with basically no problems. But I knew exactly what I was going to do before I started actually coding. The (significant) time leading up to that was spent more-thoroughly understanding what and how I wanted to do, and at some point it all clicked in an "oh. so that's how. OK, might as well build it now" moment.
Also your only option when working with other developers.
But yes, it absolutely compounds the issues. Everyone involved has to thoroughly understand it all / their role in it, and getting to that point likely takes longer than discovering it as you go :)
> "discovering how to program a thing" and "programming something you already understand".
Understanding the problem is key, as others have said. It's my belief that we seldom understand the problem in any detail until we've basically written a working system, and we'd do that fact the most justice by beginning a second draft as soon as the first working version is 'done'. That generally won't fly in the workplace, and that's one of the main reasons I avoid the workplace.
No, neither have. You misunderstand the algorithm suggested. Even if you had 0 bugs, you're still going through the process described. The overwhelmingly common case you then describe:
> When I'm done, it generally compiles and runs fine after about 20 minutes of fixing silly bugs.
How is this not exactly what the article describes?
> Programming is a long slog of trial and error, where the length of the trial and the
> severity of the error depend heavily on the domain and the tooling.
This article describes the idea of an interactive programming environment with a single language for all problems.
This method of development, as described in this article, is very common in industry but not very productive. It is still lot of trial and error and in that same time I can be doing something that I know I will do correctly.
there are plenty of people programming in datflow languages where you do exactly this (eg LabView, Max/MSP, PureData, vvvv, etc...). Guess what: after some time it just becomes shit too, because making such graphs is freakin hard.
exhibit A: http://1cyjknyddcx62agyb002-c74projects.s3.amazonaws.com/fil...
exhibit B: https://ni.i.lithium.com/t5/image/serverpage/image-id/184872...
I've done that quite a few times too, and found it to be faster than trying to "design as you go" and having to constantly debug and make incremental changes to fix things (which also tend to have the effect of making the code messier.) If you think everything through and then write the code, the only bugs tend to be minor, spelling-related and such, but otherwise the code usually "works the first time".
I also find writing a plan helpful if only enumerate the issues at hand. It always changes but its good to start with.
I find generally this approach leads to less production crippling errors.
https://github.com/LiveAsynchronousVisualizedArchitecture/la...
With those paramaters it would take about 23hr to type. Luckily I have an IDE, I comment a lot, and I indent and make a lot of whitespace to separate ideas between lines.
Not my cup of tea, but sorta plausible.
Hence more work has to be done on expressing solutions to big problems as the composition of solutions to smaller problems. Which is fundamentally an algorithms problem.
> Current abstraction methods are subpar: they require inherent complexity, are language specific, and are not easy to change after you've using them (unless you have adapters on every part of the code base which in it's own right becomes a mess).
Programming languages exist to implement algorithms, which in turn exist to solve problems. If your language of choice is getting in the way to implementing the algorithms you need to solve problems, you have to switch languages, not anything else.
Wherever it makes the most sense for the algorithms you want to implement.
> interactions between components
Again, driven by the needs of the algorithms, and, most importantly, their proofs of correctness.
I think it is. A framework is a pattern of behaviors. You have inputs, transforms, and outputs. Some are connected, some you leverage by use case - standard library of a utility or core namespace (e.g. from flask import jsonify)
In the meta sense, you might be able to come up with an algorithm that makes connections automatically, but then...it is meta.
Unifying algorithm and architecture has been somewhat of a holy grail of PL, being able to express your whole program (including your frameworks) as just procedures would be very convenient, but no one has figured out how to do that.
If a software framework doesn't have idioms, I'm not sure it's a framework. Examples of frameworks that have no case for using it dont do well.
This is by its very nature a less deterministic solution than a pure algorithm.
Better abstractions for solutions are great, better abstractions for problems would be even better, but I'm not sure they'd help all that much for understanding difficult problems... perhaps more data on the problem would help, but that's often lacking.
IOW, the mental version of BDUF (Big Design Up Front).
> For a multitude of reasons, straight-line, sequential imperative code comes more naturally to programmers than functional/declarative code in their conceptual program model
On the contrary, I think most people are 'configured' to think declaratively and functionally. Many programmers on the other hand are somewhat mentally atypical in that they think quite imperatively. This leads them to pursue technical hobbies, like programming. However, we do a huge disservice to think that 'humans' are better at imperative stuff. In my experience, there's a significant subset of people that find declarative stuff significantly easier, but do not pursue programming when they take their first OOP course and are turned off.
For me at least, I played around a bit with programming when young, but it never clicked for me until i started exploring the declarative and functional languages. These just came way easier to me than everything else, and had I not been exposed to them, I doubt I would have continued in this as a profession.
But the problem is, programming isn't about just putting down a first order encoding of your needs. It's about bridging the gap between that encoding and the libraries actually available to you.
That's where declarative programming becomes unintuitive to people. How do you bridge the gap between your declaration and the declarations provided by Rails/Vue/Webpack/etc? You need to somehow imagine the transformation that will get you there.
Imperative programs, on the other hand, always have a ready axis for decomposition: time. You break your program up into tiny time slices, and then work backwards to find procedures that that get you to the first one, then the second one, etc, until you hit the end of your program.
With declarative programs, you need to slice the program in an abstract space. In my experience it takes 6-12 months to get up to speed with a new declarative programming landscape like Rails or Ember.
I used this video to get a better understanding - I hope it helps others too:
Insightful comment. When using libraries, we always use the API in an imperative way. Even if the library uses a declarative model, we pass around declarative data via imperative API calls. Is this because imperative is somehow more natural and easy? Or is it is because the fundamental cross library binding model in a C/Unix world is imperative only?
In a different world, what would a declarative binding model even look like? If the system provided a declarative binding model (e.g. by exposing a library as set of bindable data flow cells, instead of a set of callable functions) perhaps integrating with declarative libraries might be easier?
E.g. most of my coworkers prefer itty bitty steps in longish methods (where I feel like the point is lost in the noise) to functional programming style compound expressions where the result/goal is on top and the details nested.
This fits real life: we can use English for casual gossip, highly specific technical documentation, and everything in between.
Another important dimension for gradual languages is difficulty: Languages with advanced verification capabilities (eg, Rust) would be much easier to pick up and get started with if you could trivially have sections of code where you didn't even need to know about the memory management features of Rust (it would be way easier to choose Rust as a primary language for a company without having to worry nearly as much about the new engineer onboarding cost).
Also, since he phrased this as an HCI problem: tooling strikes me as just as important as language design. A language that was gradual between some sort of highly constrained drag&drop interface and text-based programming would be great.
This seems to, to an extent, describe SQL.
TFA does all of the above, plus a parenthetical saying "inference is addressed in the next section" -- and then does not actually address inference later in the post.
I'd much rather have type inference than optional typing.
Having said that, I now really like Rust which goes all the way in the other direction.
Well, your reasoning skills are different from your compiler. You can see things that the compiler can't. But the compiler can also see things that you don't until the compiler points them out to you.
> ... and I can thus determine that certain designs are type-safe that my compiler cannot.
True. But your compiler can also see that certain things are not type-safe that you think are.
Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it.
Very true.
> Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it.
For me, it depends on the language. If you have generics, macros, and non-nullable types: I'm on board. If you lack any one of those, I'd rather be dynamic. I don't want to be constantly overriding the compiler, writing a lot of boilerplate, or still have to deal with nulls.
double sum(double[] numbers) {
double total = 0.0;
for (int index = 0; index < numbers.length; index++) {
total += numbers[index];
}
return total
}
Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `numbers.length >= 0` (established by the implementor of the array type) imply it.
Inductively assume that prior iterations of the loop preserved the invariant and didn't perform any invalid indexing operations. Now, every time the loop's condition is evaluated, there are two possibilities: either `0 <= index == numbers.length` or `0 <= index < numbers.length`. In the former case, the loop terminates and no further indexing operations are used, establishing the claim. In the latter case, `numbers[index]` is a valid indexing operation, and the subsequent `index++` operation does not destroy the invariant, because, given the precondition `0 <= index < numbers.length`, the operation `index++` establishes the postcondition `0 < index <= numbers.length`, which implies the invariant.
---
Note, however, that in this case it would have been more efficient to use an iterator, because the iterator's implementation already packages this proof in a reusable way, so that you don't need to reprove it every time you write a loop similar to this.
---
@winstonewert
> True, but the key word is "can". I could write a proof that my dynamically typed programs are correct
If you could actually write the proof, then you would not want the dynamic checks, as all they offer is protection against errors that you can prove you have not made.
> or that my functions do not index out of bounds, but I don't.
Are you actually sure you can?
---
@AnimalMuppet
> By a certain point, you've seen enough of them that you don't have to prove it, you can just see it.
If all your loops are so similar to each other that you can “just see” that an iteration pattern is correct, you should consider writing an iterator library, so that others can benefit from your hard-earned wisdom without going through the pain themselves.
Or else, if you are implying that you could be given an arbitrary loop and “just see” that it is correct, I am afraid you are wrong.
> But of course, everybody thinks they're at that point well before they actually are...
I have never even entertained the possibility.
Even if I write a formal proof, I'm not guaranteed that my program won't index out of bounds. Formals proofs have errors in them all the time. I want dynamic checks to catch me in those cases.
Further to the point, let me reiterate: programmers do not (in almost all cases) write these proofs you are talking about.
> My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot.
Anyhow. Back to your last comment:
> Even if I write a formal proof, I'm not guaranteed that my program won't index out of bounds.
If you actually come up with a proof, you are completely guaranteed that the proven statement is true.
> Formals proofs have errors in them all the time.
Correction: Purported proofs often actually aren't proofs. It is not a proof if it is wrong.
> I want dynamic checks to catch me in those cases.
Thanks for making my point for me! Self-quotes are decidedly not tasteful, but this situation calls for a reminder:
> It is useful (again, according to proponents, not me) to consider these inconsistent attempts valid programs so that programmers can obtain example-based feedback about the consequences of their designs. Logic and abstract reasoning are not everyone's forte, after all.
Anyhow. Back to your last comment:
> Further to the point, let me reiterate: programmers do not (in almost all cases) write these proofs you are talking about.
This is just a statement of fact, which is true, indeed. But it doesn't support your original position in any way.
The purpose of HN is to gratify intellectual curiosity, not smite readers with the same harangues over and over again. If you don't want to be banned, you're welcome to email hn@ycombinator.com and give us reason to believe that you'll use the site as intended in the future.
Yes, in the strictest sense an incorrect proof is not a proof. But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. You cannot be unaware of this point. You must have understood what was being conveyed. Yet, instead you decided to engage in a nitpick over the meaning of the phrase "formal proof"
Furthermore, your claim that "If you actually come up with a proof, you are completely guaranteed that the proven statement is true." is utterly unhelpful. You know that my point was that a manually verified proof might still be wrong. And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof.
So at this point, you are not discussing the questions in good faith, and I'm done with this conversation.
(And no, I'm not backing off my position.)
They are wrong. A purported proof is only a proof if it is actually correct. If you cannot reliably come up with a proof, not mere purported proofs, then just be honest and say so. We are not in a consultant-client relationship, so you gain nothing by lying about your skills to me.
> You know that my point was that a manually verified proof might still be wrong.
Only if you cannot reliably come up with correct proofs.
> And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof.
It is not an “ill-considered nitpick”. It is essential to my point. If you can prove that your assertions hold, you do not need to check them dynamically. (Of course, this is logically a triviality, and it is awful that I need to explicitly make this point.)
But of course, everybody thinks they're at that point well before they actually are...
Java has a particularly bad type system, and it used to be even worse.
> Another big question in gradual programming is inference vs. annotation. As our compilers get smarter, it becomes easier for information like types, lifetimes, and so on to be inferred by the compiler, even if not explicitly annotated by the programmer. However, inference engines are rarely perfect, and when they don't work, every inference-based language feature (to my knowledge) will require an explicit annotation from the user, as opposed to simple inserting the appropriate dynamic checks. In the limit, I envision gradual systems have three modes of operation: for any particular kind of program information, e.g. a type, it is either explicitly annotated, inferred, or deferred to runtime. This is in itself an interesting HCI question--how can people most effectively program in a system where an omitted annotation may or may not be inferred? How does that impact usability, performance, and correctness? This will likely be another important avenue of research for gradual programming.
This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today.
Additionally, I didn't want to dive into dynamic vs. static typing at risk of inflaming the Great War, but the point I was trying to make was moreso empirical. A huge number of programmers have used dynamic languages to build large systems in the last two decades, which suggests that there is _some_ benefit, although further research is needed to precisely quantify the benefit of dynamic languages.
Type inference demands some rigidity in the type structure of a language. You must have the right amount of polymorphism: the STLC has too little, System F has too much. If you want both type operators and type synonyms, then operators can't be applied to partially applied synonyms [0], because higher-order unification is undecidable. If you want subtyping, you also have to do it in a certain way [1]. More generally, the type language must have a nice enough algebraic structure to make it feasible to solve systems of type (in)equations, because that's how inference works.
Your post contains a link to a paper [2] that contains the following passage:
> In this paper, we present a way to achieve efficient sound gradual typing. The core component of this approach is a nominal type system with run-time type information, which lets us verify assumptions about many large data structures with a single, quick check.
I have no way to confirm this claim at the moment, but it seems entirely reasonable. Checking structural types requires doing more work. But it is this very structure that makes type inference possible and useful.
So, yes, it seems that inference and gradual typing will be difficult to reconcile.
---
Footnotes:
[0] http://cstheory.stackexchange.com/questions/32260/ (I am the author of this stupid question.)
[1] http://news.ycombinator.com/item?id=13781467
[2] http://www.cs.cornell.edu/~ross/publications/nomalive/nomali...
> Gradual programming is the programmer tracking the co-evolution of two things: 1) the syntactic representation of the program, as expressed to the computer via a programming language, and 2) a conceptual representation of the program, inside the mind. In the beginning of the process, the programmer starts with no syntax (an empty file) and usually a fuzzy idea of how the final program should work. From this point, she takes small steps in building components of the program until the final version is complete.
calls to mind things like the B-Method (https://en.wikipedia.org/wiki/B-Method).
Here you first specify your program at a very high level in logic; then you refine the model, still in logic, and proving that the refinement is valid; you iterate some more refinement steps, i.e., you gradually make parts more concrete by actually implementing individual operations; and at the end you have a complete, executable program. A program that, since you proved all the refinement relations as you progressed, is also formally verified against its spec.
Of course this is too much work for most domains, and many domains don't even have any useful notion of formal specs. Also, the actual B system is a horrible thing with a horrible logic and horrible proof tools. But the general idea is appealing, for some things.
(0) without destroying the safety guarantees of typed code,
(1) correctly assigning blame, if a runtime type error happens, to the specific untyped part of the program that causes the error.
Common Lisp's optional types don't quite fit the bill.
(check-type foo string)
When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...
You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion).
> When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
Your method seems impractical in the extreme in a commercial team environment.
Most people do not want to make/take many decisions, especially for things they dont care (in that moment), so they go for something that has those predefined. As +/- , usualy that something comes with lots of other extra decisions predefined too.. and the pain starts. Sooner of later u want full control of some aspect, and in order to get yoursefl free on that aspect, ... u have to either do horrible hacks, or re-make everything yourself. And there is the other extreme. Next time, u'll just start there. With No gravity defined - whatever that brings (like very long schedule. Or very loose language).
Usualy people take magnitude(s) fewer decisions-per-minute than what one needs in programming. Same for alternativity. Hence the difficulty of programming..
And yes, the all-or-nothing approach that is all-over software, has to be anathema-ed. For 30+ years, i have not seen anything good in it. i want to be able to choose-and-mix (which is, decide) by myself. And so do my new pupils.. And all the intermediate levels. Just the set of aspects, and details thereof, is very different for me and for them. Which calls for even greater graduality-flexibility-alternativity..
Myself, i have ended doing everything in python, for it stops/chains me the least, without getting too unstructured. Usualy making little "languages" for anything that i might, all on top of each other, "gradualy" changing the semantics; away from the language predefined, into the target domain. And, generating all else that cannot go this way.
have fun
I was already 8-9 months into coding with over 10K lines of code before I added ASDL schemas for the AST [1].
I believe this was a good thing, because I had running code from the start, and the only way to understand shell is over many months. It's impossible to just "think about it" and come up with the correct schema. The schema follows not just from understanding the language, butfrom the algorithms you need to implement on the language. [2]
So I see the value in both -- starting out with a very loose notion of types, then making it stricter.
I'm taking the next step now and am looking to make that detailed schema static rather than dynamic [3].
[1] Success with ASDL http://www.oilshell.org/blog/2017/01/04.html
[2] From AST to Lossless Syntax Tree http://www.oilshell.org/blog/2017/02/11.html
[3] Building Oil with the OPy Bytecode Compiler http://www.oilshell.org/blog/2018/03/04.html
(copy of Reddit comment)
What's nice about T-SQL is that you can do a lot of your programming in it and then you generators to generate all your C# code (Query-First) and even your client side code (I'm working on a console app that will do that for me). But the tooling for this is not very mature. I don't understand why programmers don't embrace it wholesale. I feel like I'm always writing so much cruft in my day-to-day job and screaming at the computer that I could do what takes an hour in C# in 5 minutes in SQL.
SQL is a bit harder to learn at first. But the more you work with it the easier it gets. And it is much easier to understand since there isn't much to it, unless you are doing something really complex. But then, I don't know if C# is that much clearer.
I just wish the tooling were as nice for PostgreSQL as it is for SQL Server. I don't understand how you can pay $200 for a product that can't even figure out what fields my alias refers to.
This is not entirely true. The author of the Gradual Memory Management paper you cite is currently building [1] a systems programming language called Cone [2] that incorporates these mechanisms. Although much work remains to be done, the online reference documentation does go into some detail about the syntax and semantics for references, allocators and permissions.
[1] http://github.com/jondgoodwin/cone [2] http://cone.jondgoodwin.com
I do think there are good research opportunities in these ideas, e.g.:
* Type theoretic work on formally proving the soundness of the mechanics (as a follow-on to the proof work done with Pony and Rust-belt).
* Cross-allocator comparative studies of performance and other factors (although many such studies have been conducted in the past, the fact that you can control for the language/runtime and even test hybrid memory management strategies would make a new study a worthy addition to prior work).
* Assessing the impact of borrowed references and lexical memory management on tracing GC's "generational hypothesis"
In your role at Stamford, perhaps you can inspire students to pursue such projects. My focus is devoted to real-world results, but I would be happy to offer support, if that would be of any help.
For any newby programmer, recursive programming is a difficult concept to grasp. Then during an intermediate programmer's stage, you realize recursive programming's power and lean on it because of it's often theoretical beauty and often simple. As you advance more, you realize the computational disadvantages (exploding stack) and softer disadvantages (lack of readability).
Would "gradual" programming ban recursive programming?
Given that Prolog dates back to 1972, I wonder if spreadsheets count as a big new idea? How about programmer notebooks like Jupyter?
Basically they're "just" a declarative data-flow system. Similar timeframe, but slightly earlier, at least as far as my wikipedia-fu is suggesting[1], in the 60s.
But yeah, they've been awfully transformative after that, and continue to be. I can't really think of a better counter-example at the moment.
* type inference
* message passing concurrency
It's a problem of education, and business needs affecting education.
What do schools teach? Python? Java? C? A little lisp maybe? Javascript (oh god)?
Why? Why are we pretending those languages have anything at all to do with learning computer SCIENCE? More like job-training for big companies, so that graduates are 'job-ready' when they graduate.
You don't need studies, because users don't KNOW what's going to make their lives better, other than incrementally better. Imagine asking people who rode horses what they'd like to have improved in terms of transportation. Who in the world would say a car? A self driving car?
Cars require massive infrastructure investments. Programming language research and development requires serious investment, and serious collaboration. When people who don't do research, decide on allocation of funds, demand X number of papers published that rot behind paywalls, etc etc, why is anyone wondering why we're still using C for critical world-wide infrastructure?
For someone who expresses this far better than I can, watch a couple of videos of Alan Kay on youtube.
Let me try and do a better job this time around:
I believe, then, that viewing programming languages (PL) through a lens of human-computer interaction (HCI) is the most critical meta-problem in the field today. More than ever, we need surveys, interviews, user studies, sociologists, psychologists, and so on to provide data-driven hypotheses about the hard parts of programming.
I agree that tooling for programmers is awful - I disagree that it is because we haven't done studies. My point was that studies will absolutely not help, for anything but incremental improvements that hardly matter. I also don't think it's the most critical problem - I'd agree that it is the lowest hanging fruit, however.
Meaning, I think there can be significant improvements to programmer tooling, within the next 5 years, and I also think the problem again lies in funding, programmers not willing to pay for better tooling (lack of imagination) and lack of imagination of the big companies.
One glaring example of lack of imagination is our current state of using the internet - html/css/javascript in a web browser is a completely broken paradigm and yet, no big company has done anything to actually fix it, some spend millions of dollars each year to keep it going in fact! Thousands upon thousands of people have spent optimizing, writing libraries for, and using a fundamentally mediocre language. That does not give me much hope frankly.
I am being quite negative so let me propose what I think is the future of programming languages: a dependent type system language with incredible documentation, standard library and an ability to drop down into a language like rust, for pieces of code that need performance.
The current trend of Swift/Kotlin is imho a syntactic and minor improvement over Java/C#, and moving in the direction you've mentioned - I think object oriented programming, dynamic languages and mutable state by default, or even having to think of managing memory, are ideas that will only be used in niche circumstances 30-40 years from now. OO for UI, dynamic languages for what bash scripts are currently used for, managing memory via rust for performance critical apps.
This is all assuming we wake up and start reading scientific papers from 30-40 years ago and actually using those ideas, rather than cherry-picking ideas to glue onto a fundamentally broken existing paradigm.
One last thought - these are all thoughts of someone who's frankly quite uneducated. I'd love to know what people who actually design languages/compilers/proof assistants for a living think.
Your vision for the future seems to be focused a lot on a strong type system, which is a reasonable bet. A lot of the people in the PL community share this view. But why? Do we _really_ need the additional benefits on top of existing type systems? Personally, I'm not yet convinced. I think helping people transition from untyped to typed code is a more important problem than building ever more complex type systems, since it's a problem people have much more frequently in the real world. Not only that, but _they will continue to have it_ for the foreseeable future, since transitioning from dynamic to static typing is a natural and inherent part of the programming process (which is also why I disagree that dynamic languages will become a niche).
But either way, both these views are still mostly based on our personal experiences. I don't think either of us can strongly claim that pursuing gradually typed or dependently typed languages is more important until we can accurately characterize the needs of programmers in the large.
Sure they have. Google wrote Dart and tried to get others on board. Then asm.js arose, allowing other languages to be compiled and run reasonably efficiently. Nowadays there's some consensus around Webassembly.
Regarding HTML/CSS, canvas and WebGL both bypass them.
It is the platform itself - meant to display static text content, being coerced into some frankenstein that requires never-ending libraries and tooling to do what desktop apps did 20 years ago.
It is hard to see any other world, so let me link you to a guy to whom it was obvious the web browsers stink decades ago.
Let me start by addressing Xanadu; you obviously get the web's folly, so I don't understand why you'd link to a criticism of the web that has been outdated for twenty years. Yes, as you point out, the web is a pile of hacks, but those hacks haven't been bolted on to add two-way links or transclusions, but - as you point out - to do what desktop apps do. Had Xanadu won over the web, someone would have created JavaScript and a bunch of hacks on top of that just the same.
A closer vision to what we've been trying to achieve is Alan Kay's, which said that browsers should have been essentially a basic layer - not an application - to run third-party code safely.
And in my opinion, webassembly and canvas+webgl are essentially that - a simple bytecode VM and two slim layers over core graphic APIs. Sure, you need some HTML to load them for historical reasons (although surely a "manifest" file format would rapidly arise to replace it), but they are essentially standalone and quite basic. All the layers of hacks are in HTML's advanced features, in CSS and in JS. Once you have applications that don't use those, you can build a browser which is just a very basic HTML parser tied to a bytecode VM.
(I think) It's not because of brains or abundance, it's because of the human language.
> How far should we go to match people’s natural processes versus trying to change the way people think about programming?
Economically, it is your time (of one person only) versus the time of potentially thousands of users. What do you think?
> How impactful are comments in understanding a program? Variable names? Types? Control flow?
Ideally, I think, comments would not be contained in the source code, polluting the general vision of its structure, but would be placed outside, as documentation.
For variable names, as long as its meaning/use is made immediately clear on first sight, without needing to figure out its frequency pattern or see its declaration to figure it out (maybe placing it in a separate place from the code, again), the variable name shouldn't matter much (as long as its not purposefully unrelated or obscure).
I think it would be useful to have something like a "live documentation" in a REPL (commands like man commands documenting each part of the language (and program), each word an entry, non-sequentially accesible). That is something I would do if I were to design a programming language, a structure called a "dictionary" documenting each and every reserved/defined word in the environment.
I believe Donald Knuth, who introduced Literate Programming, would disagree with this.
"According to Knuth, literate programming provides higher-quality programs, since it forces programmers to explicitly state the thoughts behind the program, making poorly thought-out design decisions more obvious. Knuth also claims that literate programming provides a first-rate documentation system, which is not an add-on, but is grown naturally in the process of exposition of one's thoughts during a program's creation."
https://en.wikipedia.org/wiki/Literate_programming
https://www-cs-faculty.stanford.edu/~knuth/lp.html
I have not used full-fledged Literate Programming, but I find having part of documentation interleaved with code helps improve both and reduces cognitive load required to search for relevant documentation elsewhere.
The main problems I've had with literate programming are:
- It has a very high risk of being very slow going. If you have to change something, then you will often find that you need to change a lot of prose.
- Because of the previous point, there is a tendency to do a lot of up front design and spike a lot of code to "get it right" before you commit to writing the prose. There's no particular problem with that except that it places a very high cost on change. There is considerable incentive to accept a sub-optimal situation because changing it will be extremely expensive.
- It is quite difficult to write prose in a reference style. Generally speaking, one is encouraged in literate programming to write your code in "presentation order". In other words, the order that you would discuss things. This is fantastic if someone is sitting down and reading your code from scratch. It makes it difficult to find the wheat in the chaff when you are debugging, though.
- Because of that, I find that I'm more often reading the undocumented code rather than the documented code -- because once I understand what's going on it's far easier and faster to just read the source code. Jumping around between the generated code and the presented code is often frustrating.
Having said that, I've found that I really like programming in a literate style when I'm writing a blog post, or the like. Because I'm thinking more in prose than in code, it works extremely well.
My personal suspicion is that Knuth had great success using literate programming for TeX precisely because he was more concerned about describing algorithms for typesetting than he was about writing a great typesetting system. I love TeX (and I'm one of the few people who actually has considerable experience using TeX without LaTeX), but it is a horrible language that works exceptionally well. In many ways I think that it demonstrates the issues that I've had with literate programming.