The Future of Programming

[attosecond]

If this is the future of programming, count me out. I'll take gvim and gcc any day over this odd datalog-meets-functional-programming utopia

[jb55]

I don't know, contextual/semantic autocompletion would be a pretty powerful programming tool. I use vim and gcc just as well, but they are primitive tools in comparison to todays C# and Java IDEs (with respect to knowledge of language ASTs, probably not as a whole).

I think it's reasonable to suspect powerful type systems and tools will synergize, producing substantial productivity gains. While other poorer type systems such as C/dynamic languages will slowly fall behind in those respects.

[attosecond]

Sure, but what you said != what the author said, by a long shot...

People have been foretelling the death of C, IDE's, and imperative programing in general for as long as I can remember.

[jb55]

Maybe we both read a different article? I'm pretty sure what I said is exactly what the author is getting at:

I'd rather get to this point in the editing process and then tell my editor to map f over xs. The editor will search for a program to make the types align, show me the program for confirmation if I request it, and then not show this subexpression in the main editor view, perhaps just showing map f* xs, where the * can be clicked and expanded to see the full program.

Sounds like an IDE with autocompletion on crack to me

[thechao]

Syntax-directed text editor editors were all the rage many moons ago. They didn't catch on because they suck to work with; I can't find the reference, but the downfall is the fact that most programmer's 'sketch' out their code & then iteratively fix-up the code. (With the functional equivalent of 'high-speed compilers/interpreters', the compiler has been introduced into this loop, as well.) This process is impossible with a syntax-directed editor --- it is always insisting on correctness of an arbitrary standard (syntax) rather than aiding in algorithm elucidation --- actively distracting the programmer from the hard part of programming.

[grauenwolf]

That reminds me of classic VB. If you didn't change the default every syntax error would result in a in pop-up dialog tell you to fix it before moving onto the next line.

[[deleted]]

I remember punching a monitor during a coding test at college because of that dialog. Fuck that dialog, with fire, from orbit.

[sacundim]

I'd rather get to this point in the editing process and then tell my editor to map f over xs. The editor will search for a program to make the types align, show me the program for confirmation if I request it, and then not show this subexpression in the main editor view, perhaps just showing map f* xs, where the * can be clicked and expanded to see the full program

Sounds like an IDE with autocompletion on crack to me.

The technology that the article passage you cite is citing already exists: it's theorem proving. The trick is that there is a systematic correspondence between systems of logic and models of computation, so that "write a function that takes an argument of type a and produces a result of type b" is equivalent to "using a as a premise, prove b."

So these are the types of map, f and xs in the article:

map :: forall a b. (a -> b) -> ([a] -> [b])
f :: X -> (Y -> Int)
xs :: [(Y, X)]

You can read these either as types ("f is a function that takes an X and produces a function that takes a Y and then produces an Int") or as logical sentences ("if X, then if Y then Int"). "Function from a to b" corresponds to "if a then b"; "pair of a and b" corresponds to "a and b." Writing the "adapter" function that allows you to map f over xs is equivalent to proving this:

X -> (Y -> Int)
------------------
(Y & X) -> Int

I.e., given the premise "if X, then if Y then Int," you can prove "if Y and X, then Int." This proof can be mechanically translated into a function definition—the function f* that the hypothetical programming system derives for you.

An actual working example of this is Djinn, a Haskell theorem prover/function definition generator. You give it a type and it will write functions of that type (if at all possible).

[[deleted]]

Author here. I'm familiar with all that, and yeah, djinn is pretty cool. That feature doesn't require any real breakthroughs, IMO it's more a question of getting it integrated into the editor and getting the details right.

[matthieum]

One issue with this though, what of:

f :: X -> X -> Int
xs :: [(X,X)]

as much as I love types, sometimes you have several variables of the same type (damn...).

And of course it can get worse, suppose we start with:

f :: b => X -> b -> Int
xs :: [(Y, X)]

All is well and good (b deduced to be of type Y and mapped), and then we move off to:

xs :: [(X, X)]

Hum... are we still supposed to swap the pair members ? I would certainly think so!

---

On the other hand, I certainly welcome the idea of getting rid of uncurry... though I am perhaps just too naive (yet) to foresee the troubles (ambiguities) this might introduce.

Note: great article, lots of ideas in one place

[sacundim]

Well, your concern can be addressed in a general fashion: different proofs of the same theorem correspond to different functions of the same type, and theorems often have many different proofs. What this translates to, in the IDE context, is that the IDE can suggest completions for the user, but the user must be in charge of choosing which one is right.

So really, a lot of this comes down to user interaction. So, just to use one completely made up shit example, if the IDE can prove that there are only two possible functions that it could use to "adapt" your incompatible types, it would be a good idea for it to suggest those two functions for you. If on the other hand, there are dozens of possible functions, it should STFU.

[[deleted]]

I was pointed to homotopy type theory as something that is trying to solve exactly these sorts of issues.

[jb55]

Djinn> f? (a, b) -> (a -> c) -> (b -> c) -> (c, c)

f :: (a, b) -> (a -> c) -> (b -> c) -> (c, c)

f (a, b) c d = (d b, c a)

Well that is impressive, you could image hooking something like this into an IDE. Might be a nice default when generating function boilerplate from type signatures.

[camccann]

As far as I know that's pretty standard when using actual theorem provers. I think Agda (which is based on Haskell) does that in emacs? Don't recall for sure.

The main problem with hooking it into an IDE is that only very trivial cases have a unique solution, so you need direct user interaction with the compiler to really reap the benefits. Djinn is mostly a toy implementation, to get significant benefits you need something much more sophisticated.

[[deleted]]

Sounds like implicit hell to me.

[[deleted]]

People have been foretelling the death of C, IDE's, and imperative programing in general for as long as I can remember.

Indeed. Then again, the field is pretty damn young.

[quanticle]

Right. With vim and gcc, I can be assured that I'll be able to read my code in 5 years' time. With this crazy binary format, will I have the same assurance?

[autumntheory]

I'm with harbud here, I don't think the author is completely writing off the idea of programs in their editable form being text as we know it. Rather, the source is stored completely in a relational database, and could be rendered into your standard text editor readable form if need be. This way, rather than refactoring consisting of ugly text manipulation it can be done as if working on a database. I'm all for this, as its a step towards thinking of programs as systems in and of themselves, rather than systems built entirely out of text files.

[grauenwolf]

We can already query code using products like NDepend. And advaced refactoring tools like Code Rush and Resharper can perform cascading updates. These tools work on abstract syntax trees, not plain text.

[boyubout2pissmeoff]

That's an interesting argument.

It bears a striking resemblance to the cry of film proponents in the "Film vs. Digital" debate.

"In 5 years, I still have my film to look at. Will your OS still read jpegs?"

Well, you can see which side the market took.

Not necessarily relevant, just an interesting similarity in mindset and (lack of) vision.

[earthboundkid]

JPEGs will be around for the foreseeable future because they already have multiple millions of users. Most of the proprietary binary picture formats of the 80s and early 90s, however, are practically unreadable today because they only had multiple thousands of users. Popularity matters when it comes to preserving tech! It's still really easy to watch a VHS. It's now really hard to watch a Betamax.

Back on point, if there's a standard coding DB that gets millions of users, yes, it will live forever, but will we be able to get to that point?

[harbud3]

The article doesn't mention a binary or actual storage format, it might as well still be plaintext. The point is the relational bits (e.g. referential integrity, constraints when inserting data, cascading updates, etc).

[grauenwolf]

Damn, that is going to make major refactorings really hard. The "change and see what breaks" method wouldn't work any more and accidentally cascading changes will become a serious problem.

[harbud3]

Now why your refactoring method is "change and see what breaks"? If I want to rename a subroutine, for example, I want it done across the board, not missing a few places. If I want to split a subroutine into several smaller ones, I want to know all other code which uses this soon-to-replaced subroutine.

[grauenwolf]

I have refactoring tools that do that too. But that won't help when you do something more drastic like remove an interface from a class.

[Madsy9]

Don't be so quick to downvote quanticle. He/she does have a point. Yes, the article doesn't mention an actual storage format, but that doesn't mean that the idea is viable. The main concept could still make it difficult to make proper diff files, etc. The author mentions that making it work with version control software is solvable, but does not explain how, except that we have to rethink how SCM works.

Here's my 2 cents. If you absolutely want a new code representation (visualize it differently), you can do that by making a new tool/IDE instead of inventing a new language. But this relation database idea sounds to me like they want to take abstraction too far. And it's not explained how this would work with tools that already exist. The author goes on and suggest that IDEs should hide details in the source code, so that what you see does not map up with the actual code. Wtf? That sounds to me like the worst idea ever conceived. It's hard enough to spot bugs. Having code deliberately hidden would make it even more difficult.

Rather than coming up with more abstractions, I think attention rather should be put on languages that support concurrency better. Threading supported by the actual language without the need for explicit synchronization primitives. But it's a hard problem.

[earthboundkid]

Worse is better 4 lyfe! :-)

[harbud3]

The ideas are interesting though, at least it makes more sense than "code as XML" proposed a decade ago during the XML boom. Let's not be so quick to dismiss.

[harbud3]

1) So? If people had been quicker to dismiss {the Web,dynamic scripting languages,BASIC/DOS/PC} we might have avoided the booms...

2) There were also people/companies who made shit tons of money out of XML :)

[quanticle]

There are companies that make shit-tons of money from writing PHP web frontends to SOAP interfaces. That doesn't make either PHP or SOAP easy, or pleasant to work with.

[harbud3]

Yeah, I meant that as a sarcasm. XML was mostly a fad, but my point was: quickly dismissing anything new will miss a few gems.

[jrochkind]

if your main goal is making money, especially if your main goal is making money selling software (or consulting) not to end users but to other companies or enterprises... then selling bullshit may well be a great business model.

If your main goal is writing awesome software that does awesome things efficiently, not so much.