Live data from Hacker News

I want to fix programming

jonbho.net

151–160 of 163 posts

Re: I want to fix programming

#151
post #112

So imagine you define some amazing PSL (Problem/Solution Language). It let's you "Code" by defining the problem and solution, ie: Define SORT: Given SET(x), Find SET(y) Where [For i in y] y[i]>y[i-1]. So now you're feeling all giddy because this amazing language is so awesome--you didn't have to specify how to do something step by step. You just declared what you wanted, and it gave it to you. Fantastic. But then, no…

No. You're thinking imperatively. The pure form would express something like: "given the property sorted(s) defined in this way, let s be a set such that for all elements e of s, e is an element of the program input. Then let the output of the program be the list l such that sorted(l) is true.

>No. You're thinking imperatively. The pure form would express something like:

>given the property sorted(s) defined in this way

    "Prompt SET"
>let s be a set such that for all elements e of s, e is an element of the program input. ... such that sorted(l) is true.

    "SORT SET"
>Then let the output of the program be the list l

    Display SET.
You've changed the wording and grammar, but you haven't stated anything different.

Re: I want to fix programming

#152
post #68

The quality of the comments both here and the author's blog is astonishingly good, every comment adding something to the discussion. This is the hacker news I know and love.

Yes I'm amazed with that too! And really enjoying it myself!

Re: I want to fix programming

#153

The problems the OP wants to solve are formally undecidable and reducible to the halting problem. 1. Given a formal specification, find a program that meets the specification. 2. The apparently simpler problem of checking whether a given program meets a specification. Both are undecidable. That said, there is an extensive literature on practical approaches to this problem. They generally suffer from intractability. h…

I agree with the sentiment that the problem the OP brings up is difficult, but bringing up the halting problem here seems pretty pedantic. If you restrict yourself to a turing incomplete language, checking a specification no longer reduces to the halting problem. In fact, there are many systems that do exactly this, and most of these systems are perfectly capable of sorting a list and proving that the list is sorted.…

You are right, I'm not intimately familiar with all the research out there and with all the details. I do think I have some useful things to add, that a "practical" angle is missing in many approaches, and that many attempts fail just because they get lost in trying to achieve theoretically elegant solutions, rather than building practical tools.

At least, I'll learn a lot. At most, we get something new with the help of other people.

Re: I want to fix programming

#154
post #116

As it happens, computer science is exactly about those rigid steps of how to get a computer do bigger things. If you could express what you want, you could replace considerable part of Knuth's books by referring to "just sort these numbers for me", leaving the "how" to the computer. Bridges don't get built because some guys "wants to go see the other shore". Bridges get built by rigorous design and constructed a rive…

I totally understand and concur with the need for the tools to build bridges by rigorous design. I also think we can look for better tools to build bridges, if we understand better the seas and rivers we are crossing, and if we analyze the limitations of the current tools.

Re: I want to fix programming

#155

I'm convinced that IF you can make this work, it's the future. 'Programmers' will still do what they currently do... But instead of writing applications, they'll be writing compilers. (Or whatever we end up calling the programs that turn declarative code into programs.) This will lead to a rise in a new job. Instead of coding, they'll be describing applications. And done right, it should be easier than coding. Initia…

I'd say IF or WHEN we can make this work. It's a task for us all. I think both academic and practically minded developers need to collaborate, which doesn't happen often enough.

Programming will remain tough and only doable for certain types of people. But I think it can be a much more pleasant experience.

Re: I want to fix programming

#156

I think we're overlooking the fact that programming is hard per se. A program runs on a computer which is nothing more than a calculator with storage and peripherals. In the end everything is just numbercrunching. The whole point of a programming language is to overcome the "old days" where you had to use a computer for what it IS, namely a calculator. We did quite well regarding hiding stuff but as a consequence we…

Programming will definitely remain hard and thought-requiring. I just don't want to waste another minute of my precious life thinking about edge-conditions at the start and end of a list or array. And I don't want anyone else to do so either. I'm sure we'll get there some how, although it definitely may not be me, but doesn't stop me from giving it a try!

Re: I want to fix programming

#157

Earlier quoted context omitted.

I don't think there's any inherent problem with stuff being declarative. We just need the software to be smart enough to handle it well. We might have a long way to go till we can do this effectively. I'd suggest looking at 'declarative' from the point of view of delegation (not in the technical sense, but the usual sense of getting someone else to do a task for you). Ideally you want to specify what you want to be d…

"We just need the software to be smart enough to handle it well." You just shifted the complexity with one sentence, it doesn't make it any easier.

I never said anything about making it easier.

I was pointing out that it's a worthwhile longterm goal, but one that requires sophisticated software to achieve.

Re: I want to fix programming

#158

The problems the OP wants to solve are formally undecidable and reducible to the halting problem. 1. Given a formal specification, find a program that meets the specification. 2. The apparently simpler problem of checking whether a given program meets a specification. Both are undecidable. That said, there is an extensive literature on practical approaches to this problem. They generally suffer from intractability. h…

The problems the OP wants to solve are formally undecidable and reducible to the halting problem.

While this is true in general, our current "solution" to the problem - hire a human programmer, give him the spec, and set him loose - doesn't do any better here. The problems we as an entire field "want to solve" are, in general, formally undecidable and reducible to the halting problem, but we get by anyways because it turns out that you can get a lot of useful work done even without solving the general problem.

I see no reason that a well-designed system couldn't similarly leverage "special cases" that are not undecidable. How efficiently this could be done is another matter, but I think step one in that direction is to accept a pretty major loss of generality - after all, that's how humans get the job done, and for the most part we're still able to turn most of the specs that we're faced with into working code, given enough time.

Re: I want to fix programming

#159

Earlier quoted context omitted.

Clojure. Clojure's lispy (simple implementation, syntax), FP (reduced state), easier concurrency, agents + stm are all influenced by this paper.

That seems like a huge stretch. Lisp has nothing to do with that paper, and minimizing state and complexity could hardly be more obvious design concerns. The concurrency aspect I can't comment on, but it's not a major theme there either. Perhaps I just don't get it, but I'm a little miffed at having tried several times to absorb the gems of wisdom in that paper and come up with nothing that isn't obvious (even the id…

The paper was about several things:

1) accidental complexity is the source of a large number of bugs 2) implicit, unnecessary, tightly-coupled state is the cause of a significant number of bugs. 3) mostly-functional programming reduces the amount of state in 2 4) RDMS databases, with transactions and triggers, are a good way of reducing state as well

Clojure applies all of these lessons. lisp reduces accidental complexity in the language. FP reduces accidental complexity wrt to state. the STM and agents are close analogues to DB transactions and triggers.

"even the idea of functional programming over relational data is obvious". Yes, but where else has that been tried?

Re: I want to fix programming

#160

Earlier quoted context omitted.

That seems like a huge stretch. Lisp has nothing to do with that paper, and minimizing state and complexity could hardly be more obvious design concerns. The concurrency aspect I can't comment on, but it's not a major theme there either. Perhaps I just don't get it, but I'm a little miffed at having tried several times to absorb the gems of wisdom in that paper and come up with nothing that isn't obvious (even the id…

The paper was about several things: 1) accidental complexity is the source of a large number of bugs 2) implicit, unnecessary, tightly-coupled state is the cause of a significant number of bugs. 3) mostly-functional programming reduces the amount of state in 2 4) RDMS databases, with transactions and triggers, are a good way of reducing state as well Clojure applies all of these lessons. lisp reduces accidental compl…

I posted a reply, but decided I was repeating myself. Thanks for the discussion.
Post reply on HN