> 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.
I don't know about others but I've done this quite a few times. When I have to write some code for a personal project of moderate size (10k LOC) I like to just sleep on it for a while, stay up very late, chug some coffee, and write the entire program. After that I click compile and run a few times, fix any variable names that I've undoutably misspelled, and then maybe 1 or 2 bugs. It's basically delaying starting a project until you have a perfect mental image of what that code needs to do, how it looks, and understand mentally every tradeoff you're making. I wish I could do this with larger code bases but unfortunately, from my own experience, planning time is exponentially related to the projected lines of code. A 5K to 10k LOC project usually takes me on the order of 2 weeks of thinking. If you go higher than that you're talking about months.
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).
Yeah, I'd call this the difference between "discovering how to program a thing" and "programming something you already understand".
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.
Making it so this isn't true with multiple developers is one of the benefits of waterfall-style programming. Design an API up-front, divvy up work, build it. As long as the design is good and you don't do stupid shit, it's entirely possible to work in parallel without getting in each other's way.
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 :)
Yes, I've done that quite a few times too. Write code for 1-2 months straight without ever compiling. When I'm done, it generally compiles and runs fine after about 20 minutes of fixing silly bugs. That requires designing the system on paper (actual paper) in quite a lot of detail first. But other times I start with a skeletal outline of input - middle - output, and evolve the middle in small increments, refactoring along the way. In either case, I always write about 5 drafts of everything at every level - the method level, the class level, and the system level. And I consider that my secret weapon - the writing of 5, sometimes 10, drafts.
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 live programming which is something that dates back to some of the older programmers. It's a common methodology that crops up often. It's not about the number of times it takes you to run something or finding spelling errors. Fixing spelling errors still counts as "running the first time" as long as you're not changing the structure of the code.
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.
Note that isn’t the meaning of live programming, at least according to the definition laid out in Chris Hancock’s 2004 dissertation where he introduces the word. Of course, other definitions have been created to include more conventional programming practices (e.g. in Lisp and Smalltalk) or performance oriented live coding, but we are all talking about significantly different things at that point.
> 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.
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.
Just because it hasn't worked before doesn't mean that there isn't a good way, that has yet to be created, for describing data flows and modularizations of systems.
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".
Extreme Programming has this idea of a "spike". It's throwaway code that you write just to figure out how to do something. (The name comes from trying to "nail something down", I think.) That's not quite just thinking for a sprint, but it's in the same direction.
You're not serious about writing out 10kLOC in a day, though, are you? I think the most I've ever managed in one day was <2kLOC, and that's already an extreme outlier.
Let's say comments make up 10% of my lines, white space makes up 10% of my lines, and a single } makes up another 10% of my lines. That makes 7000 lines. Let's say every line is filled with 80 characters that I have typed (no auto indent). Let's assume there are 5 characters in the average word and I type at 80wpm.
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.
OK, I can see that by the numbers it is possible, if you have planned everything so well that you don't waste any time getting stuck or rewriting. While I do this for much smaller amounts of coder, 10k LOC is so much that I don't think I could possibly plan it out that well, and also keep it in my head. Personally I find that my plans fall apart once I actually start to write out the code and notice many things I forgot, and usually I find the code is much uglier than expected and I try to find better ways.
> I wish I could do this with larger code bases but unfortunately, from my own experience, planning time is exponentially related to the projected lines of code.
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.
Not everything can be done through algorithms, actually, a lot of programming involves just designing parts, where to hold state, interactions between components, basically what is called architecture.
That is a very simplistic 1D view of programming. Quicksort is an algorithm, algorithsm are often reused. A UI framework is not an algorithm, and it is most definitely if you are writing a UI.
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)
You have those, but you don't have core algorithmic property of an effective method that can be computed within a finite amount of time and space. It isn't even very meaningful.
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.
Don't be dense. How a controller in an MVC framework maps to a url and provides an execution path through the framework is an algorithm. The fact you plug in multiple values to make that happen (including the executing function) is the idiom that results in a consistent algorithm. You can alter this, which isn't a compelling argument.
A UI framework is better understood as an algorithm plus a psychological model of your user. You must understand what they are thinking at every step of the way, guide them to the answers they want, and help them avoid pitfalls.
This is by its very nature a less deterministic solution than a pure algorithm.
Is it the complexity of the solution (LOC), or complexity of the problem?
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.
>I don't know about others but I've done this quite a few times. When I have to write some code for a personal project of moderate size (10k LOC) I like to just sleep on it for a while, stay up very late, chug some coffee, and write the entire program. After that I click compile and run a few times, fix any variable names that I've undoutably misspelled, and then maybe 1 or 2 bugs. It's basically delaying starting a project until you have a perfect mental image of what that code needs to do, how it looks, and understand mentally every tradeoff you're making.
IOW, the mental version of BDUF (Big Design Up Front).
Which, for a small system, can work, because you can hold the whole design in your head, and because you can write the whole thing before any requirements change. Try to scale that up, though, and you get into the usual BDUF disasters.
> 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.
You're right people's first thought tends to be declarative.
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.
Thanks. I’ve been following this sub-thread with interest. I have very little theoretical understanding of the differences between imperative and declarative (functional) paradigms.
I used this video to get a better understanding - I hope it helps others too:
> Imperative programs, on the other hand, always have a ready axis for decomposition: time.
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?
Well, yes, our current implementations of computation ultimately are all imperative, which explains the preponderance of imperative thinker in the programming field. However, this is an implementation detail. Had the first processors been declarative (as they very well could have been, when you think of thing like automaton chips), we would have seen things play out differently. My point was that making broad generalizations like the one above automatically shuts out a large portion of the potential programming community.
To be clear, I mean that in an empirical sense more than a prescriptive sense. More people use imperative code than functional code, and one hypothesis is that it's simpler for people to think in terms of instructions. But as I mentioned earlier in the post, that's purely a hypothesis which should be the subject of further research!
Good thread here. Good topic for a “multiple kinds of intelligence “ type study.
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.
Gradual programming certainly strikes me as the future of programming. I see the end goal as being able to use a single, unified language for every application. Certain sections of a large codebase might need their own special jargon or abstractions; but that shouldn't necessitate a totally separate language and toolchain.
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.
It seems to me that the languages we write programs in today are generally at the wrong level of abstraction in one way or another. Imagine if we wrote long-lived programs in a sort of lingua franca pseudocode, and then compilers competed with each other over the years to produce ever more efficient machine code from that well-established pseudocode. In this fantasy world, for example, Adobe Photoshop isn't written in C++. It's written in logic. They keep writing new features in logic-language, and at the same time their compiler team keeps working to make a better compiler that produces a better compilation target.
> Imagine if we wrote [..] in a sort of lingua franca pseudocode, and then compilers competed with each other over the years to produce ever more efficient machine code from that well-established pseudocode. In this fantasy world [..]
This is where I think Python 3.6 has made a significant leap forward. Optional type annotations help bridge the gap between the phase where you're trying to understand the problem space, and let you grow it to something production ready.
I am in general deeply skeptical of gradual typing, partially from my own underwhelming experiences with MyPy, and partially because 99% of the time when I hear someone advocating for them, they (1) take as given that dynamic typing makes for more productivity (which does not reflect my own experience), and therefore don't try to justify the claim at all, and (2) they say what gradually types give you is not having to annotate things up front. Types have not required manual annotations since at least 1978 (the original hindley-milner type system which, I will note, while not new, is still more recent than prolog).
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.
The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are paths in the design space that lead to correct solutions but pass through several inconsistent attempts (i.e., containing parts that contradicting each other and/or the problem statement). 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.
I'd make yet a different account of the benefit of dynamic typing. My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot. This means that in static languages I end up either 1) spending a lot of time convincing the compiler my design is type-safe, 2) am restricted in the designs I can choose 3) casting types losing the advantage of static typing. With dynamic typing I'm free to just write the code.
Having said that, I now really like Rust which goes all the way in the other direction.
> My reasoning skills exceed that of my compiler...
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.
> Well, your reasoning skills are different from your compiler.
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.
This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the program's comments and/or documentation. But it does not justify dynamic typing in any way. For example, most programming languages offer no way to statically verify array indexing operations, so I just get my hands dirty and prove my array indices correct the old fashioned way (brain, paper and pen). But runtime bounds checking still annoys me, because they branch on a bit whose value I know beforehand, creating an unreachable control flow path.
Theorem: Whenever `numbers[index]` is used, `0 <= index < numbers.length`.
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.
Well, I've never seen anyone write a proof for a function so trivial. Instead, most people will simply deem the proof to be sufficiently obvious they don't need to write one out. I've only ever seen someone offer something in terms of a proof for more complex situation where its decidely non-intuitive that array indexes will not go out of bounds.
You can only deem it obvious if you can actually prove it.
---
@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...
> 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.
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.
Yes! This is the nice moment when the other party in the debate starts to back off from their original position, which, I shall remind you, was:
> 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.
We've asked you before not to be uncivil on HN or take it into tedious, repetitive flamewars like this one. Not only are you still doing it, it looks like you're using HN exclusively for it. That's not what this site is for. Since you can't or won't stop, I've banned your account.
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.
> Correction: Purported formal proofs often actually aren't formal proofs. It is not a proof if it is wrong.
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.
> But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense.
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.)
True, but the key word is "can". I could write a proof that my dynamically typed programs are correct or that my functions do not index out of bounds, but I don't. Nor has any programmer I've ever worked with. Nor has any open source project I've ever seen provide such proofs. People do not write these imaginary proofs, because it would be a waste of time.
I disagree. I've been programming professionally for 33 years. I may have written one wrongly-indexed "for" loop in the last 10 years. By a certain point, you've seen enough of them that you don't have to prove it, you can just see it.
But of course, everybody thinks they're at that point well before they actually are...
Yeah, that's an actually reasonable argument (I don't buy it either, but it's coherent enough). But I honestly think most of the time people aren't making that argument, they're just complaining about the typed languages they know -- more often than not Java.
Apologies, I forgot to follow up on the promised inference discussion in the original version of the post. I just added a paragraph at the end on my thoughts.
> 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.
> 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.
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.
> 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.
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.
Best I can tell, pretty much everything he describes is already part of Common Lisp. “Gradual Typing”, for example has a long history in Lisp, and is pretty much the default way to write programs.
Exactly. Everybody wants this incredibly expressive, powerful, functional, safe language that they dream about. We already have Lisp and nobody actually wants to use a language that powerful because it's not actually easier, especially for collaboration.
Does: it asserts the type of the place and throws a (restartable) error, giving the user a chance to fix the problematic value rather than bailing. I guess they don't really solve (1), but the stack trace that arises is a start.
Stack traces contain a lot of information. Most of it is useless garbage. Yet at the same time sometimes stack traces don't contain the information you need. Making them even more useless garbage.
What I need is the proof that the program is correct. Bugs will show up as gaps or inconsistencies in the proof. But, in the absence of even an attempt at a proof, all I can do is throw the program to the dogs.
I've never yet had the luxury of working in a language that admitted formal proofs of correctness. Do you mean informal "proofs" like unit tests?
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...
> I've never yet had the luxury of working in a language that admitted formal proofs of correctness.
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.
It seems pretty useless to even try to formally verify a program when all of the dependencies that are necessary to do anything useful are not formally verified. Where do I find a formally verified TCP/IP stack, a formally verified database, a formally verified HTML/CSS renderer, etc.?
I've found unit tests for system libraries like this before. The idea is that you run them each time you upgrade your framework, but in practise you run them every time (slowing down your debug loop) and managers use them to inflate the effectiveness of your actual tests, which is obviously measured in "number of unit tests" rather than %coverage (or, better still, %possible input values to each line)
Sorry, I proposed unit testing as a real-world formalisation of requirements in an earlier post, and you didn't contradict me. What automated system would you use for this instead?
Automated, huh? There is no replacement for using your brain, and reasoning abstractly about the preconditions and postconditions of program fragments.
So, you write down the formal requirements you have of an operating system (with aggressive auto-updates enabled, or disabled, as the customer chooses) once, on a piece of paper, and hope that they don't change?
Your method seems impractical in the extreme in a commercial team environment.
someone said "software is made of decisions". IMO this is the problem. All those listed axises, and another dozen i could imagine (esp. moving away from machine and closer to reality), they all require decisions to be taken.
Some of these decisions are predefined - from the language, OS, hardware, employment, audience, customer, tie-color, whatever. Other are obvious. But a lot are not even understandable unless one has been-there, done-that.
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.
It's amazing it took so long to get here. Obviously less smart people like myself, figure this out on our own. My brain doesn't have a lot of processing power, and I always try to shorten the feedback loop between what I write and the response I get from the programme itself, instead of throwing myself in layers and layers of abstraction. But to me and I think many others, this is the only way. We have to make the language, and flow of the code conform more to the human intuition.
Actually I believe abstraction is a tool with the express purpose of limiting the amount of stuff you have to keep in your head. Abstraction lets you omit the nasty details, so you can work with a representation of the problem space that better fits in your brain cache.
FWIW, the implementation of Oil is following a "gradual" trajectory. It's amazing how long various "wrong" things were in the codebase!
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].
I find F#'s type inference to be really nice. You feel like you are almost writing in a scripting language but whenever you mess something up it will tell you. And if you say, "No F# you are wrong!" F# always wins. And the ability to write small pieces of the code in F# interactive is tremendously useful. I find I like T-SQL for that same reason. I can write small programs scripting as I go and bring everything together in a bigger program all without having to worry about types too much. The tooling isn't quite as nice with T-SQL as it is with F# (granted C# blows F# away with its tooling, but F# is catching up slowly).
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.
> Several of the axes mentioned (memory management, language specialization) lack any documented attempts to systematize their treatment at the language level.
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.
I appreciate the clarification, as I did not catch that from the context. I just assumed maybe you were not aware of my follow-up work with Cone.
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.
Even though Perl6 isn't production ready yet, I'm surprised to see it not being mentioned in a group of languages with some gradual typing support as what I would subjectively consider idiomatic Perl6 takes advantage of quite a few things including gradual typing.
I wonder where recursive programming fits into this.
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?
Mathematica has had pretty advanced programmer notebooks for something like 20 years i think. Jupyter definitely isn't new. The only new part would be a lot of languages (Python, Julia...etc) starting to use it.
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.
I'm surprised to disagree so thoroughly with someone who teaches a programming languages course at Stanford.
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.
I'm not sure why our two viewpoints have to be at odds. I wholeheartedly agree that improving education and encouraging students to focus more on understanding the fundamentals instead of the syntax is important. But our languages are still in need of improvement!
I went off on a rant rather than address your post, I'm sorry.
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.
I think we're not seeing eye-to-eye on the HCI part here. The value of talking to programmers in the field is just to understand what are the most difficult problems they face day-to-day. You don't have to ask them how to solve it, but just getting that initial feedback is invaluable in understanding whether a proposed research direction is likely to have an impact. This may require some ingenuity on behalf of the researcher to tease out underlying causes from symptoms, e.g. if a user says "my problem is that my code breaks all the time," is that because their debugging tools suck, because they need a better type system, etc., but at least you're grounded in reality.
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.
no big company has done anything to actually fix it
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.
Everything you've mentioned completely misses the point - it is not just performance that stinks, it is not just javascript as a language that stinks - all these tools are incremental improvements that completely lack imagination.
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.
I didn't miss the point, but I may have bungled mine.
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.
pagedraw.io is working on fixing html/css(/but not js) in a web browser by giving programmers a better tool, and compiling into html/css standards (since we're stuck with them)
> Is imperative programming more intuitive to people than functional programming? If so, is it because it matches the way our brains are configured, or because it’s simply the most common form of programming?
(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.
> 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.
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."
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.
I've done it a few times. I'm now firmly of the opinion that ideally the only language you should see in code is a programming language. If you can not express the intent clearly in the programming language, then you should work at it until you can. It's not always possible and I write comments when I have to. Some languages are not very expressive, either, which makes it difficult.
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.
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).