I want to fix programming • Hacker News Board

Re: I want to fix programming

#121

Post by dullcrisp » Wed, Jan 25, 2012, 10:15 AM UTC

rmcclellan wrote: post #78

ChristianMarks wrote: post #64

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.…

Can you provide links to papers which try address this problem in practical terms, or some leads that one might use to acquaint themselves on the current state of research in this area? The paper the parent links I've only skimmed but what it seems to be advocating seems not to be that far from test-driven development. Has anyone tried anything more closely resembling what the OP is proposing? Are any such attempts doomed fromt he start?

Re: I want to fix programming

#122

Post by Gigablah » Wed, Jan 25, 2012, 10:17 AM UTC

psykotic wrote: post #40

> There was recently a very interesting post by John Carmack about static code checking, where he cited a great tweet by Dave Revell on code checking: "The more I push code through static analysis, the more I’m amazed that computers boot at all." Wrong attribution. That tweet was originally by Ryan Gordon (@icculus).

I took a course on magnetic storage technology and now I'm perpetually amazed that computers even work.

Re: I want to fix programming

#123

Post by Xion » Wed, Jan 25, 2012, 10:21 AM UTC

The assertion that programming is broken seems to be stemming from assumption that, in contrast, human minds - which currently do the programming - are not. And that's a huge overstatement. For a product of a process that is essentially throwing things at wall and see what sticks best (usually called 'evolution'), it's not that bad, yes. But it's still ridden with bugs: misperceptions, biases, reasoning errors and inconsistency.

The last one is especially relevant. Is it really so that the biggest problem of programming is putting the intent into code, because the intent itself is perfect and pure? Isn't it quite the contrary, that forming your wants into the rigorous form of code is also helping to reshape them into (more) consistent ones?

Re: I want to fix programming

#124

Post by wladimir » Wed, Jan 25, 2012, 10:26 AM UTC

nnq wrote: post #117

Why not fix the problem with 2 languages? Let me explain. You would have: 1. a language for your actual code - the real code of your application (imagine an application programmed in Python or C++) 2. a language to concisely describe what the code does - the code for your "tests" (imagine the tests written in a simplified Haskell or some dialect of mathematical language) There would be different constrains for the tw…

I really like this idea. You'd essentially have to describe the same system twice, from two angles, and the compiler cross-validates them. This is more work, but I think this will help humans understand what it does, and what it is supposed to do better as well.

And it would aid maintenance/refactoring. Behavior that is now implicit in the code would have to be written down explicitly (separating desirable behavior and side effects/bugs), and unlike "design documents" it is actually validated... (ie, a refactoring would be changing representation 1 without changing representation 2)

Separating intent and implementation, so to say. You might be on to something.

Re: I want to fix programming

#125

Post by jaekwon » Wed, Jan 25, 2012, 10:48 AM UTC

    def factor(input) = prime:
      input % prime = 0
      prime > 1

Even worse...

    def fermat() = a, b, c, n:
      a^n + b^n = c^n
      n > 2

Re: I want to fix programming

#126

Post by silon3 » Wed, Jan 25, 2012, 11:13 AM UTC

jerf wrote: post #55

So, over the years I've played with many things that claim to be "declarative", and here's why I now shy away from them like the plague. There's no such thing as "declarative". No matter what you type into the computer, at some point it's going to turn into instructions that do the thing you want done. Trying to create a declarative language is a way of making it extraordinarily opaque as to what the machine is actua…

Agreed IMO: Annotating "turing complete" code is not in any way declarative programming.

Re: I want to fix programming

#127

Post by apl » Wed, Jan 25, 2012, 11:36 AM UTC

nnq wrote: post #117

Why not fix the problem with 2 languages? Let me explain. You would have: 1. a language for your actual code - the real code of your application (imagine an application programmed in Python or C++) 2. a language to concisely describe what the code does - the code for your "tests" (imagine the tests written in a simplified Haskell or some dialect of mathematical language) There would be different constrains for the tw…

How does that differ from, say, Haskell's QuickCheck [1] and its ten thousand counterparts in other languages?

[1] http://en.wikipedia.org/wiki/Quickcheck

Re: I want to fix programming

#128

Post by nickik » Wed, Jan 25, 2012, 11:45 AM UTC

gonehome wrote: post #72

jerf wrote: post #55

So, over the years I've played with many things that claim to be "declarative", and here's why I now shy away from them like the plague. There's no such thing as "declarative". No matter what you type into the computer, at some point it's going to turn into instructions that do the thing you want done. Trying to create a declarative language is a way of making it extraordinarily opaque as to what the machine is actua…

I think to have a truly declarative language that doesn't just dissolve into obscure commands at some point requires the language to have a true understanding of human language. Which to currently do well even just for answering questions requires Watson levels of computing power.

I think human language sucks at giving commands. Yes human language is very expressive but its very easy to misunderstand each other. With code its always your fault if it dosn't do what you want, you exprest it wrongly. With human language you the error can be on both ends.

Re: I want to fix programming

#129

Post by wccrawford » Wed, Jan 25, 2012, 11:54 AM UTC

giberson wrote: post #93

timmaxw wrote: post #80

Earlier quoted context omitted.

There's a bug in your definition of SORT. The OP complains that it's easy to write imperative and functional programs that contain bugs; I don't think that declarative programs are fundamentally better.

Tongue in cheek, you don't know how PSL handles negative array bounds--perhaps it's smart enough to know how to handle the first element.

Actually, I don't see why it couldn't be 'smart' enough to know how to handle non-existant array locations. It just needs to know to handle all the valid cases, and ignore the invalid ones, and it's good to go.

Re: I want to fix programming

#130

Post by wccrawford » Wed, Jan 25, 2012, 12:02 PM UTC

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.

Initially, the 'compilers' will be pretty bad at what they do. The code they produce won't have memory leaks and such, but it'll be horribly inefficient. But thing will gradually get better and better until machines are writing better code than humans, for the majority of applications.

Eventually, as with current self-hosting compilers, new self-hosting compilers will be created and programmers will be phased out. This will be quite an interesting day.

One thing I see holding this back is computing power. The initial horribly-inefficient programs will be created by horribly-inefficient 'compilers'. They'll take insane amounts of processing power to do their jobs. Eventually, this will get better, and processing power will increase, though. It may be that we aren't at a point where it's plausible yet.