I want to fix programming | Hacker News Reader

I want to fix programming

jonbho.net

164 pointsjng159 comments

Dear Jon:

What you have is fabulous and immediately useful: You are describing a language for describing constraints on the results of computer programs.

In other words, you can express the correctness of a computer program and check whether a program is, in fact, correct.

It’s true that IF a sufficiently smart compiler could infer a working program from the definition of correctness, no further “programming” would be required. However, we don’t have that yet, and in fact I’m not urging you to write it.

Instead, consider the benefits of your language just the way it is. You can use it to write test suites. You can embed it in other languages to express design-by-contract.

It looks valuable in its current form.

Take a look at quickcheck if you want something that works today.

http://www.haskell.org/haskellwiki/Introduction_to_QuickChec...

Reg, thanks so much for your comment. I'm really happy you appreciate the value.

It's very interesting that you put the focus in the descriptive language. I've been working on that for a long time. It's not finished, but some areas are clarified. Indeed, after reading your comment I think I will try to focus on getting somewhere workable with that part first.

This whole project is so big. It will be good to do it in the open and use as much help as I can.

The "Why Dependent Types Matter" paper at http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf actually uses an implementation of "sort" as its driving example.

The paper starts out with a simple sort implementation, and then adds static proofs of correctness for:

A) Totality (Termination/no infinite loops) B) Length of output = Length of input C) Output is sorted

It does not prove the one-to-one mapping, and I don't know how hard that would be to prove (intuitively, it does not sound like it should be too hard).

The dependent types approach lets you write a program while reasonably controlling its algorithmic complexity and operational behavior -- and still have its mathematical meaning proven to match a specification.

I think a title like "I want to fix programming" is a bit over the top -- given that it is a hard problem with very smart people working at it. It is more acceptable, in my opinion, to "fix programming" after learning in detail what the state of the art already entails. That means knowing Agda, Coq, Logic languages, Hoare logic, etc.

Thanks Peaker. I know a bit about dependent types, and how complex types sytesm can help a lot. Indeed, the title is a bit over the top (or maybe even too much over the top!). Hopefully the attention will help get some extra hands & brains.

At the very least, all the pointers I'm receiving are really valuable.

I don't claim I can fix it, but I definitely want to fix it, have some ideas, and I'm willing to work, listen and learn!

And if I think I can add something, is that I come from a practical/industrial background. Most of my work has been in C++. I'm looking for practical tools for everyday work.

I once read a programming book on Elliptic Curve Cryptography, which was invented by Dr. Neal Koblitz. So the book said - whatever is in the next 200 pages is considered trivial by mathematicians working in number theory. If you write it in the form of equations, this entire book will occupy less than half a page. It is basically a lemma and a few theorems. But this book is 200 pages long. Why ? Because it tells you how to implement that lemma and those theorems using C++.

So that's how that is.

Just yesterday I described to an intern how to generate the nth term of a Halton sequence in base k. So if you want the 17th term in base 3, well, decimal 17 = ternary 122, reflect 122 to get 221, then ternary 0.221 = decimal 0.926. So the answer is 0.926. Its very, very simple. High school math. The nth halton term is in fact given by a 1-line equation in mathematics.

Now he came back with scala code to do the same thing. Look at this monster:

def Halton( n:Int, b:Int):Seq[Double] = {(1 to n).map( x=>Integer.toString(x,b).reverse.zipWithIndex.map(y=>(y._1-'0')*pow(b, -(y._2+1))).sum)}

Now it works & its functional programming & computes a million Halton terms in any base in 5 seconds and so on, but still, look at it. Is it anywhere close to the one line equation ? If I express what I want declaratively, will it be any simpler ? Not really. Why not ? Because a declaration like "1..n" means an imperative loop, a declaration like "convert 17 in decimal to ternary" means a whole bunch of divisons and remainders and aggregation, then a reflect means reversing a string, which implicitly means iterating over a character array and allocating new space for the reversed result, then a reconvert ternary to decimal means an iteration with powers of 10, where a power means other iteration over multiplication....jesus! This simple 1-line equation in math becomes hundreds of thousands of loops in practice. There's no getting around that. If you've gotten around it, you've just invented math!

I imagine that the book might as well have used another (simpler) language. Now, as I see it, to understand the math, you need quite a lot of domain knowledge. A formula doesn't make sense out of context. Most statements written in programming languages do that, in a much higher degree.

Therefore, to actually do the ECC, I think it's quicker just to read the language specification of your (simple) language, than actually understand all of the math being the formulas. Granted, you wouldn't understand WHY it works. And that's my point. Comparing math to programming languages is like comparing apples to oranges.

See Nile/Gezira: http://www.vpri.org/pdf/tr2009016_steps09.pdf

Also, the STEPS project in general (read the progress reports): http://www.vpri.org/html/writings.php

They talk about "active" or "runnable" maths. The programming languages they create aim to basically mirror mathematical expressions. This in turn makes the programming stack much smaller and easier to comprehend.

That function definition is a monstrosity because it is poorly factored. Assuming pre-existing fromBase and toBase functions, here is a definition that in my opinion is easily readable and matches your verbal description:

    halton b n = fromBase b (reverse digits) / b^(length digits)
        where digits = toBase b n

Just to show there's nothing up my sleeve, here are the fromBase and toBase definitions:

    toBase b 0 = []
    toBase b n = (n `mod` b) : toBase b (n `div` b)

    fromBase b []     = 0
    fromBase b (n:ns) = n + b * fromBase b ns

They too read like how a mathematician would define them. (I abstained from use of foldr/unfoldr to make this clear.)

Edit: On second thought, it's easy to implement it as a direct recursion. I'll demonstrate it in C so I'm not accused of language chauvinism:

    double halton(int b, int n)
    {
	return (n == 0) ? 0.0 : (n % b + halton(b, n / b)) / b;
    }

Here the digit reversal is implicit in the recursion (the oldest programmer trick in the book).

This C code is self-contained and compiles to a tiny handful of machine code instructions, so it's hard to see how your statement that "this simple 1-line equation in math becomes hundreds of thousands of loops in practice" holds much water.

The only reason it's one line in math is that the rest of math is implicitly hiding in your brainstate. If you could extract that out it would be much bigger and uglier much like your expansion of this code into loops and memory manipulation, etc.

But what's your point? Code can do more wide ranging things and does so with fewer available symbols (no superscript for pow() operations), so it's wordier, but really it's not so far different. It may take a computer 200 pages of explained C++ but it takes a child months and years of schooling.

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.

http://cfpm.org/pub/papers/tiofdm.pdf

I suggest looking at Robert Harper's book on type theory instead.

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.

However, I think the real point is that there are at least dozens of smart people who are working on this exact problem all day, every day. The OP shows neither a deep understanding of why previous attempts at this have failed or really, any knowledge at all about the state of the field of programming language research.

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?

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.

I have a question about this Christian, assume that we can accurately model an atom with a computer and then we uploaded a human into the computer, wouldn't the computer then be able to either solve the problem or report that the problem is unsolvable? I understand the halting problem but isn't there some kind of meta check that a sufficiently complex system could output?

Sure, having a virtual human try to solve the problem would be pretty good. However, even the virtual human would never be able to check the specification correctly for every possible program due to the halting problem. In particular, no matter what the specification was, a malicious user could create a program that mimics the virtual human's response and then does the opposite thing (it's the same basic proof that the halting problem is undecidable). By construction then, the virtual human would answer incorrectly when asked whether or not the program matches the specification.

So, academically, even the "virtual human" approach doesn't work since it doesn't answer correctly for every single program. Practically, you're right, having a virtual human would be good enough for most uses.

That said, I wouldn't want to use a virtual human for this due to ethical concerns :-).

The problem is that even real live humans can't always tell if something will halt. For instance, you tell me if this loop ends:

    n = 4;
    goldbach = true;
    while(goldbach) {
        goldbach = isSumOfTwoPrimes(n);
        n += 2;

You just have to prove the Goldbach Conjecture. :-)

The thing about the halting problem, though, is that it doesn't say "You can't write a program that can determine if another program will terminate". It says "You can't write a program that can determine if any other program will terminate."

Case in point: Resharper will tell me "This function never returns" in cases where it obviously wont return, and also offer to simplify methods that only ever return a single value despite what looks like a complex set of if-statements.

So, if it is possible to write a program to determine if a specific subset of all possible programs will terminate, is it possible to write a program that can generate a subset of all possible programs from a specific subset of all possible specifications?

I can't be perfect. But might it be useful?

This! That's why the halting problem is not an issue. Yes, it's impossible to solve in the general case. It doesn't mean it's definitely possible to solve it in 99% of your everyday programming work. Isn't that valuable? Isn't that worth an attempt at getting there?

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.

So long as the problem you are trying to solve is constrained by the ease with which you can express the problem, this will help.

But it will not help when the constraints are elsewhere: memory, network, CPU, heterogeneous interoperability; all still relevant in these times of mobile and distributed computing. When you are operating to these other constraints, you need control - or rather, consistency and predictability - over the consumption of those other resources. It's no good having a magic compiler that can turn your specification into an implementation, if you don't know whether the implementation will run in O(1) or O(n) space or time, what kind of constant factors are involved, and how easily you can tweak the tradeoffs when you hit one constraint or another.

I concur with raganwald's comment: this is more useful for proving, static analysis, testing, etc.

Furthermore, I'm pessimistic that you'll see substantial improvements in expressibility using your approach, particularly when you try to scale it above simple functional (by which I mean stateless input to output) problems. The reason is that programming is an exercise in attention to detail while simultaneously keeping the large in mind; and your focus won't change this fundamental nature. Writing a complete specification for a program rivals writing an imperative implementation in complexity (soup to nuts, I'm not talking about high-level DSLs here, which is an approach equally applicable to the imperative route). I expect a good compiler will swamp you with the inconsistencies of your hidden, unstated assumptions.

For example, I note that your sorting specification doesn't specify whether or not the sort is stable; I think that makes it incomplete, and also it's a tricky constraint to encode.

You are right, and I think you've found one of the weak spots. But I do think that can be treated, and the advantages of the programming-ease will be a good trade-off in many cases with the lost control for efficiency.

It's like the switch from assembly to C, or from manual memory management to automatic memory management. You lose something. You gain something else. The new approach is not valid for everything, but for some/many cases, it's much better.

Yes, the spec of a complete program will still be a great amount of work. The default resulting code will probably be slow. But you will be able to "describe" the program (in many cases), and you will be able to optimize it later without risking the correctness. Hopefully that can be a great aid and tool in many cases. We'll see, and I hope to have a lot of help along the way doing it publicly!

BTW, if what comes out is just a good new approach to static code analysis / formal specification / etc... it will have been worth it. But I do hope to find a usable tool at the end of this quest :)

I wish you the best of luck in any case. I look forward to reading more about how you expect the transformation logic would work.

He doesn't have to specify whether or not the sort is stable -- the compiler should only have to satisfy the constraints he imposes. So if he doesn't specify that it must be a stable sort, the sort might be unstable, just as with many sort routines that don't specify whether they're stable.

This is what I mean by hidden / unstated assumptions. So on one version / implementation of the compiler, a program may produce correct output, where on another, it produces incorrect output, because of a hidden assumption about the stability of the produced sort. The problem may not be found in testing due to this; and what will debugging the program look like?

If this is the kind of issue that can come up in a really simple task, what kind of issues will emerge as things scale up?

> Writing a complete specification for a program rivals writing an imperative implementation in complexity

> I expect a good compiler will swamp you with the inconsistencies of your hidden, unstated assumptions.

Thank you, this is exactly what I came here to say.

The entire practice of programming is formally defining how everything works, and the devil is always in the details. The effort of going through those details thoroughly and defining exactly what you want to the program to do in all situations is, simply, the act of programming itself.

The best you can do is create languages, libraries, frameworks to help you do it more efficiently.

i came here to upvote this comment. it touches on the real problems concisely without just sneering about reinventing declarative programming. metaprogramming is worth pursuing, but the considerations hinted at above point to why it is so difficult to realize.

one thing everyone who is hating on the idea is missing is that if one compiler somewhere finds a solution on the Pareto front, for a sub-problem, that pattern can be uploaded to the cloud and re-used by other compilers. this would over time tend to help with the practical problem of how to conserve resources in the face of such a hard overall problem.

Relevant stuff from SICP [1]:

"The contrast between [a mathematical] function and [a computing] procedure is a reﬂection of the general distinction between describing properties of things and describing how to do things, or, as it is sometimes referred to, the distinction between declarative knowledge and imperative knowledge. In mathematics we are usually concerned with declarative (what is) descriptions, whereas in computer science we are usually concerned with imperative (how to) descriptions.

...an important current area in programming-language design is the exploration of so-called very high-level languages, in which one actually programs in terms of declarative statements. The idea is to make interpreters sophisticated enough so that, given “what is” knowledge speciﬁed by the programmer, they can generate “how to” knowledge automatically. This cannot be done in general, but there are important areas where progress has been made."

[1] http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-10.html...

Yea, you will invariably run into the halting problem and similar. But I think academics are too held back by that in general. The "program space" is very large, and there's of course a lot of strange beasts out there, but only a very small subset of all possible programs are meaningful to create (in the sense that people want them or their output).

Hope springs eternal...

But so does a-historical thinking.

"Programming is broken. Completely broken."

The "software crisis" has existed since, oh, computers began, maybe fifty years ago. Which means that, in a sense programming couldn't possibly be "broken" since it never ... was ... working ...

A way to put to it is that programming has never been as amendable to planning, to the realizing one's intentions as ... we THINK it should be.

And there's the interesting part.There are lots of things that are hard for humans beings - say, flying supersonic jets or solving partial differential equations.

What's funny about programming is that we always have a hard time of it BUT we always, over and over again, think it should be easy.

There is something interesting, a study for psychologists.

I would claim that a factor is that since programs are like the natural language we normally use, we intuitively expect programs to be a "smart" as other human beings in understanding our intentions and so we wind-up disappointed over and over again.

Of this leaves "intentions" and "smartness" as defines in our model. Perhaps we can use this situation to get some clues as to their meaning...

Here is another way of defining something is sorted, taken straight from a real language:

  Inductive StronglySorted : list A -> Prop :=
    | SSorted_nil : StronglySorted []
    | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l).

What this says is that an empty list is sorted (SSorted_nil), and that given some sorted list l, if a is less than all of the elements in l (well, we generalize to some relation R), then a prepended to the whole list is sorted. (SSorted_cons)

But it turns out, there is another way we can say this property, if our relation is transitive: all we need to say is that the element is less than or equal to the first element of the list.

And for any non-trivial specification, there are literally dozens of ways of specifying it, all of which happen to be identical. Which one do you pick? Which one is easier to use? Hard to say, in general.

Source: http://coq.inria.fr/stdlib/Coq.Sorting.Sorted.html

http://www.cis.upenn.edu/~bcpierce/sf/ is a good way to learn coq if you are interested and don't already know it.

also, i didn't completely follow the final example, but you might find that category theory is relevant. related, it's not completely clear to me why you're not happy with functional programming. in a sense what academic functional programmers are doing is what you want your software to do. they're just not smart enough to put it in a compiler yet. i think. for example http://www.fing.edu.uy/inco/cursos/proggen/Articulos/sorting... (isn't that kinda what you want?)

The most common declarative programming language used in SQL. In theory the optimizer takes my declaration and builds an optimum (or at least decent) set of step in the database engine to accomplish what I have declared. With all the work in this limited area, database optimizers get it really wrong quite a lot (Sybase 12.5 was bad enough on big data that forcing order of joins and indexes was needed).

I am not sure we are at the stage where the computer can be trusted with the "what". Most new learners need to be told step by step the "how" and computers seem to be at that stage. Prolog is a nice counter-example, but even it can get itself into some real trouble.

I agree programming is broken, and I agree the whole program knowledge is just painful, but I am think there are some steps before full declarative. As much as I dislike the old VB, it did have a very vibrant component market. That concept didn't seem to evolve or make it to the server. I look at Mongrel2 and wonder if the component approach could be applied. Regardless, I think the biggest problem is lack of ability to separate the pieces of a big project effectively no matter the eventual solution.

The most common declarative programming language used in SQL.

Or maybe a spreadsheet (http://philip.greenspun.com/panda/databases-choosing).

although I respect Philip Greenspun greatly, most spreadsheets I have seen are pretty procedural. People tend to think in steps on those types of calculations.

For those who haven't read it yet, this paper has a lot to say about the cause of programming complexity, Out of The Tarpit:

http://web.mac.com/ben_moseley/frp/paper-v1_01.pdf

They say that the only essential complexity is the one inherent to the problem the program is trying to solve. Everything else is just here because we haven't yet found the methodology or invented the tools to battle it.

They also describe an ideal world, where all the programming is done in way of declarative programming - what you want the code to do, and not how to do it.

So I am relatively naive when it comes to declarative programming in general and have not yet read this paper (I will after commenting here), but that said...

Don't you have to (at the very least) tell the compiler how to do things? To reuse the example from the article: when you tell your friend to get you a beer, at some point your friend has learned HOW to get you a beer. Similarly the compiler will need to know HOW to do things that you declare. Sure it will be great when we can just tell the compiler that we need this list sorted in reverse alphabetical order but at some point someone is going to have to program the sorting algorithm on the back end.

Am I way off or are we just talking about a hypothetical future when compilers are (even more) black boxed and we don't have to think about them anymore?

Declarative languages are defined by the fact that in them, you don't tell the compiler how to do things. You just describe the result you want, and it's the compilers job to get there. Yes, this makes the compiler rather hard to write.

SQL is probably the primary example. Prolog is also well-known.

For anyone who may not know, Prolog does this in a pretty interesting way. You have some declarations that make up your program, Prolog takes these and then uses them to conduct a logical proof (like in discrete math). You negate the premise (proof by contradiction), and then try to show that this will cause a contradiction (line 5 says Bob is Human, but line 42 says Bob is not Human). If you can find such a contradiction, your premise was true.

It does this by using backtracking, which is really interesting in itself if you're not familiar with it.

Also fascinating is the amazing and innovative virtual machine that drives Prolog: the Warren Abstract Machine.

See: http://wambook.sourceforge.net/

Great paper. I'm familiar with it, and I think it's one of the initiatives out there pointing in the right direction. Same as Prolog and SQL. But we still have to work a long way in that direction for it to pay off nicely in our day to day!

this paper has a lot to say about the cause of programming complexity, Out of The Tarpit

This paper is highly regarded by some smart people, but every time I've tried to read it I've seen nothing of much value - only some obvious platitudes about complexity (including the bit about complexity being intrinsic to the problem vs. just the implementation), a lot of architectural gobbledygook (complete with boxes-and-lines diagrams), and some hand-waving about combining the functional and relational models. Has anything ever come of this? Specifically, any working systems?

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 idea of functional programming over relational data is obvious) and that couldn't have been said less pretentiously in easily a tenth of the space - ironically, for a paper about minimizing complexity.

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?

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

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 actually going to do. It looks great in four lines, it crashes and burn on any real sized problem, because you inevitably hit the following sequence:

1. I encounter a problem; a performance issue or a bug.

2. I can not practically proceed past this point because everything I might need to figure out what is going on has been "helpfully" obscured from me.

Yes, you can still thrash and flail but this hardly constitutes a "fix" to programming. You simply can not help but create an abstraction that not only leaks like a sieve, but is actually multiple leaky sieves layered on top of each other in opaque ways. (And letting us see in is in its own way a failure case too, with these goals.)

Part of what I like about Haskell is that it helps bridge the gap, but doesn't actually go too far. A map call is still ultimately an instruction to the machine. It's not quite the same type of instruction you give in C or C++, what with it being deferred until called for (lazy) etc, but it's still an instruction and it can be followed down to the machine if you really need to without only marginally more work than any other "normal" language. (It may be a bit bizarre to follow it down all the way, but hardly more so than C++ in its own way.)

Contrast this to SQL, which is declarative, and you never have to worry about what the database is doing to answer your question. Except it never works that way and you inevitably must actually sit there and learn how indexes work and how queries are parsed and how the optimizer works to a fairly deep level and then sit there on every interesting query and work out which synonymous query will tickle the optimizer into working properly except that you actually can't do that and you end up having to turn to weird annotated comments in the query specific to your database and then you still end up having to break the query into three pieces and manually gluing them together in the client code.

And I don't even care to guess how many man-millenia have been poured into that declarative language trying to make it go zoom on a subproblem much simpler than general purpose computing. (Well, except isasmuch as they've more or less grown to encompass that over the years, but it's still at least meant to be a query language.)

So, if you think you can fix that problem, have fun and I wish you the very best of luck, no sarcasm. This is the problem I've seen with the previous attempts to go down this route before, and I feed this back in the spirit of helping you refine your thoughts rather than yelling at you to stop.

What if you created a declarative language which allows you to override the algorithms in a functional/imperative? You could create a public algorithm repo that auto-pulls into your local machine on setup. Could search for algorithms by declarations. That would be a lot of reuse.

> What if you created a declarative language which allows you to override the algorithms in a functional/imperative?

We have that. They're called libraries. If I need to sort a collection, I don't write an imperative chunk of code, I just do:

    sort(myCollection)

Looks pretty declarative to me.

The issue here is that function definition doesn't tell what the function does. So you may have hundred implementations of sorting algorithms in different libraries, and neither compiler nor the IDE know that they all do the same thing. So when you write

sort(myCollection)

you are still referring to one particular set of instructions. The system parent poster envisions (the way I understand it) would be along those lines:

* User gives SPECIFICATION of sort, along the lines OP writes about in his blog.

* Other contributors provide various implementations which satisfy the specification. Such system would either have to auto-prove that implementation meets specification or just trust contributors that it does.

* Then in your code you can write sort(myCollection) and the system would pick the best implementation.

Interfaces, polymorphism and templates?

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.

Quantum computer might open unexplored doors.. :)

Best answer so far :)

> Trying to create a declarative language is a way of making it extraordinarily opaque as to what the machine is actually going to do. It looks great in four lines, it crashes and burn on any real sized problem,

Erlang, Haskell and Ocaml are examples of declarative languages, and they all have been used to solve very real-sized problems: telecommunication switches, compilers, trading systems, a window manager, etc.

It amazes me how the argument above is still repeated (often followed by "but those systems don't count, give me an example of X".)

I love OCaml, but I would hardly call it a declarative language. You still describe the steps to perform an algorithm, rather than the result of the algorithm. The article poster references Haskell and explicitly says "The functional approach brings indeed several improvements over regular imperative or object-oriented programming. But still it’s not the solution."

The argument forwarded for considering them declarative is that their compilers perform transforms on the source code, and that there are no side-effects.

I certainly agree with your interpretation more. Typical functional programming isn't really declarative (though, yes, moreso than imperative programs are) and those waters shouldn't be muddied.

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 done and you shouldn't care about how it's done. Software is meant to be a labor saving device.

I assume you're ok with the idea of delegating tasks to people. If the software was smart enough I think it'd reasonable to delegate to it as well.

Search is declarative and works well.

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

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

SQL is declarative, and that's it's strength. The optimization, indexing, and other tweaking of the implementation is separated from the code that declares the result needed.

I'm not convinced you can really separate those things in a practical context. Inevitably you end up with a leaky abstraction and the opaqueness of what's actually going on makes it harder to diagnose.

I think declarative is the right default, since it shows the intent over the mechanics, but I deeply distrust any system that won't let me be very specific about the mechanics if I need to be.

The problem is not that SQL is slow, the problem is people push the system until it becomes slow.

It's just as easy to write 'JOIN this billion row table with that billion row table' as it is to forget how hard that is. We may complain that creating indexes is painful, but take some huge complex and slow query and try recreating it in C++ correctly and at least as fast and you quickly enter a world of pain.

PS: It's awesome to be able to write something and then optimize it without worrying that you are going to break something. When it comes to efficiency being able to select performance trade-offs even in an arcane fashion beats testing everything from scratch by a huge margin.

The problem is that most SQL engines have commands for fine-tuning. Things like 'ignore index', for instance. That is a leaky abstraction - knowing the details of the system lets the programmer do better than the query analyzer. Similarly, sometimes a left join + null check performs better than a "where not exists ()" subquery, despite them serving identical purposes.

If you can change how you phrase a query and get different performance, while keeping the same semantic meaning, your language isn't just leaking, it's hemorrhaging. It may still be useful, perhaps world-changingly so, but it's a perfect example of the dangers of declarative programming.

As to 'try making it in C++': with a library for doing so with as much maturity as SQL? Sure. It'd probably be reasonably simple, if more verbose. And when it inevitably runs slowly, you can infer the reason for why A runs faster than B relatively simply, because it's doing precisely what you told it to do.

You have a point, declarative approaches almost never delivers as promised, which is "you don't have to worry about implementation".

In reality, as you say, you end up with edge cases where you still need to dive into the implementation in order to find out what's happening.

I don't think it's a good enough argument to dismiss the whole paradigm though. Im prefectly happy with my declarative regular expressions that work 90% of the time, and rather take the hit debugging those hairy 10% that end up not working well, than writing my own imperative parser every time and repeatedly deal with those off by one errors etc..

When you say "it never works" I suspect you really mean "it never works in 100% on the cases".

Jerf, thanks so much for sharing your thoughts. I think I agree with all your views. They are taken from the real experience of trying those approaches. And I am grateful that you provide the feedback. I and anyone tackling this steep mountain need all the help we can get.

I am sure that inspectability/debuggability are two of the big issues with such an approach. When things fail, the more magic there is, the more difficult it is to fix it. It's even difficult to understand what's happening!

I do think that there is a gap there. You can specify things and have the environment apply your spec. If it's totally naive, like Prolog's "slowsort", it will take exponential time and be impractical for real-world cases. But if strategies can be found and/or devised, and applied, which get some efficiency, it can be practical for many things. When things fall apart, it's clear that powerful debuggers will be needed. A lot of work will be needed on the tools, similar to SQL Query Strategy Inspectors, etc... maybe even professionals specializing just in this. But I think that it will finally allow us to write code in a sane way. Even if armies of professionals have to come after the fact to tweak it so that it's usable, the same as for SQL.

I totally understand what you see as adavantageous in Haskell. I think that same "it's turtles all the way down", where you can inspect and debug every step, is the reason that Haskell cannot gain the power that I am after. Prolog can't either, for other reasons.

I believe a fundamentally different approach is needed. And that's what I'm trying to sketch out.

And thanks to you and many other people hopefully we can learn whether there is something there or there isn't, and if there is, hopefully reach some useful result!

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?

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 rivet by rivet or bolt by bolt. Then you can go see the other shore.

For most part, we've come a long way in programming. Sorting has many reasonable algorithmic approaches well-studied and as a result of that in almost any language you can already say sort() and have some stuff sorted. I don't particularly need to know that Python uses timsort, it just sorts. Of course, I can study sorting in detail if I want to and possibly discover something novel.

Why programming never gets easy is that by solving existing problems we accumulate newer, more complex problems and interactions. Programming will always be difficult because we automate anything that's no longer difficult.

The "Sort these" example is not programming, it's something else that potentially builds on programming. Type some stuff into Matlab and watch your computer sort out difficult stuff for you and do the calculations in parallel in highly efficient manner using Cuda. It's not programming, it's using a machinery that has been programmed to interpret certain classes of the user's wishes and take care of all the physical steps required to finish the desired computation. You still can't ever take a blanko computer, ask it to sort stuff, watch it figure out how and call that programming.

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.

“Computer generate for me the sequence of all possible steps I could take; highlight moves that results in high economic and emotional payoff. Feel free to use alpha beta pruning and dynamic programming to reduce the time taken to polynomial time. Also, constrain possible moves to reflect my personal proclivities. Also, highlight a path were I'm dating Alicia Keys and Drake is with Nicki Minaj.. hate to see him beg on a music video.” [1]

My dream programming language should be able to run this. Good luck.

[1] http://chestergrant.posterous.com/your-favorite-programmer-d...

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 two languages, as language (2) would not have to be efficient or portable or any other requirements you can imagine, it should just be very concise, to allow to describe in a couples of lines what 100 or 1000 lines of language (1) code do.

And it would be very different from just writing very granular tests: the program could be run in "debug" mode, with the language (2) tests or executable-descriptions of a function running after every function call (very slow but still working), and in a "real" mode in the client computer or when profiling and optimizing for speed. You could still have regular test and language (2) could be much simpler than something like Haskell because it would not need have fast execution and it will only be written in short snippets that could be proven correct by "pen & paper" or "mind running".

[minor edit for spelling and paragraphs]

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.

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

Thanks, I took a better look at that and realized there are 2 implementations of QuickCheck for Python... I'm not really a Haskell developer so I didn't knew much about QuickCheck.

Though I still think none of our current programming languages are good "test" languages... I just gave Haskell as an example, but there are probably tons of things that would make it annoying for writing descriptive versions of an algorithm that could be used as tests...

And at least the Python version of QuickCheck I just looked at are far from a descriptive "implementation" of a function... they seem more like some test-automation that could only prevent most of the bugs that might not crop up in typed language...

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.

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.

Isn't the beer example somewhat self-defeating? It seems to me that the only reason we don't need to tell our friends how to get the beer is because he has already those concepts abstracted away, but he still had to learn them, mostly by imitating others, but also by being explicitly taught.

Sure, he didn't have to be taught how to fetch a particular kind of beer in a particular house, but then again, when I make a new e.g. Starcraft map, I don't have to change the code to teach units to move from a coordinate to another. The learned algorithm is just general enough that it applies to any object that fits a certain interface.

And humans make a lot of errors to correct their internal spacial navigation algorithms. To correctly fetch a beer, it took years of bumping into stuff and falling down until the algorithm was robust enough.

Seems to me that a system with hand-written imperative algorithms and a general mechanism of iteratively improving them by trial-and-error is much more close to what we humans to than a compiler that simply comes up with algorithms from scratch from just reading intents and goals.

As CPU excess increases, I guess I've always thought that eventually code blocks could be grown using genetics inspired algorithmic processes that could just try everything possible until something works well.

Sounds like you're talking about genetic programming: https://en.wikipedia.org/wiki/Genetic_programming

It took the universe 13.7 billion years and an ever-expanding memory space; I'm not entirely sure if this is the right approach…

Isn't that just BogoSort? :) http://en.wikipedia.org/wiki/Bogosort

To some extent this is already done in a process called "Superoptimization"[1]. In that case, though, correct code is used as a rigorous functional specification, and the Superoptimization process will replace segments with shorter or faster opcode sequences with identical side effects.

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

You are underestimating the rate at which the number of possibilities to be searched explodes exponentially. Read the paper on Denali, an optimizer that conceptually tries all possible instruction sequences to compile a piece of a program optimally. Even though they used sophisticated pruning techniques and state of the art combinatorial solvers it didn't work for anything beyond a couple of instructions (less than 10), and AFAIK nothing practical ever came of it. Say you can currently successfully synthesize instruction sequences of length 6. The thing with exponential growth is that even if computers became a million times faster, then you might be able to achieve instruction sequences of length 9, not of length 6 million.

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!

This doesn't look much simpler to me, and I suspect the problem with this approach will wind up being incomplete or overconstrained specifications, rather than incorrect programs.

To use the language of the op, it will be composed of many discrete simple assertions that excruciatingly specify the output.

This is called declarative programming (http://en.wikipedia.org/wiki/Declarative_programming), as opposed to imperative programming.

Sure, sorry, didn't mention on the article, Prolog is the closest thing that exists, although I think Prolog commits at least one cardinal sin that breaks the really great properties (/cut/) and it just doesn't get deep enough.

Prolog is a kind of declarative programming, but the two concepts are not the same. From the link: "declarative programming is a programming paradigm that expresses the logic of a computation without describing its control flow." This can be implemented in any way one desires.

You probably already know this but you should really save yourself a million comments and put an update in the article that shows you already know about Prolog. :)

Also see Mozart/Oz and other constraint programming systems. http://en.wikipedia.org/wiki/Constraint_programming

Came here to say this.. the language already exists!

Not to discourage you from trying anything but it looks like you've ignored the complexity issues with this (I won't pick at the fact that you described an O(n^2) algorithm for sorting).

I understand that you don't want to specify the steps to achieving the goal but the steps directly impacts running time.

In your particular example, a compiler could produce a program with the correct output but runs extremely slowly even for small arrays (by simply trying all permutations until it finds one satisfying your constraints, or even worse, randomizes the entries until the constants are satisfied ("bogo sort")).

Furthermore, there are undecidable problem for which the output is easy to specify but no program could exist. For example, deciding if an input piece of code will loop indefinitely.

In your article, you've mixed needless overhead (the dummy/local swapped variable comes to mind) and the steps needed to specify an algorithm.

If you only want to remove the overhead (and thus, some source of mistakes you've pointed out), you could aim for a language where the algorithms are easier to specify.

In the bubble sort case, the code would look something like.

  def bubble_sort( array ):
  	while there is an i such that array[i]<array[i+1]:
  		swap( array[i], array[i+1] )

(You can almost do this in Python already which seems to be where the syntax is inspired from. I can elaborate if interested.)

Ultimately, I have to agree with other comments saying this will be more useful for checking than specifying a program.

[EDIT: fixed code formatting]

You already said you will be looking and SQL closer, so let me give a few pointers here.

Consider that in SQL you specif how to store data, including indexes, and then what you wan to get, but not how to get it. In other words you specify data structures and the engine picks a set of algorithms and builds an execution plan. The next logical step would be for the user to specify the schema, while the database engine is not only choosing algorithms but also reshapes your data into data structures that would allow optimal algorithm selection later on. At first it would only build new indexes, but then it could also start employing partitioning and ultimately move to normalization/denormalization.

Secondly, be on the looklout for when a problem reminds you of a SQL query. For example, a mail application looks like a query where you specify which fields from which emails you want to see and in what order, and on top of that query result you're specifying a style sheet, CSS on steroids, to make it render pretty. Style sheet is also declarative, not imperative! I am presently working on a framework that follows this model to facilitate iPhone app development, and it's looking pretty good already.

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 lost control over parts of the machine. Setting a pin on your LPT-Port on high in Python? Just no. Doing the same thing in this guys "language"? I don't know if that will be included or even possible (if it is please tell me).

But in the end you're still writing code for a calculating machine. Things will never be as easy as "Sort this array by comparing each element for size" because the underlying hardware still is the same. Unless you figure out how to make that easier, for example by intorducing a "qsort [array]" assembler instruction within a processor, that has hardwired Quicksort logic, you're going to stay where you are: In the low-level lands of C and FORTRAN with some nifty little masquerades, like Python, for the same stuff all over again.

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!

http://lukepalmer.wordpress.com/2012/01/19/sentences-and-par... is an interesting look at parallels between declarative programming (as in Prolog, or in jng's pseudocode language) and functional programming in languages like Haskell or ML.

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, now that you have defined this "SORT" routine, you still need to use it. You end up with the following code:

    Prompt SET.
    SORT SET.
    Display SET.

Shit! You're defining steps again.

You ultimately can never achieve your goal, because you will always need to define some steps. All programs of significance are a composition of tasks which need to be identified, and executed.

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.

It has a much, much worse bug than the negative index: your definition of sort says "given x produce a y which is sorted and completely unrelated to x in any way". The implementation "given x return y=[1,2,3]" satisfies your specification...

The negative index issue is a valid bug concern because when I was typing out the _fictional_ PSL code I missed the negative index hence my reply that said language could be smart enough to handle that (ie, tongue in cheek). However, your bug is not legit, because you've introduced extra wording for an assumption you can't make since you're not the creator of my fictional language. For PSL, "Given SET(x), Find SET(y)" implies that SET(y) is a resultant set of SET(X). SET(y) could have a case where the elements are different than SET(x) but only where explicitly indicated by the requirements. The requirements specified by the where clause in this case do not dictate a transformation on the elements, only a re-ordering. So no, it's not a bug.

It's funny that despite it being a passing pseudo example to make a point about programs being compositions of tasks that I'd be this vested in defending the code correctness of my pseudo code but I can't help it.

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.

What I'm pointing out is that "steps" are arbitrary; they're not intrinsic properties of the system. You can express the entire program as a definition tree without ordered expressions.

Jon, you're looking for haskell. But there's a catch -- programming in haskell is HARD, and expert haskellers are the best of the best, thus EXPENSIVE.

many customers don't want correct programs, they want cheap programs. Some people in finance care about correctness, maybe you should check them out.

Dusting, thanks for the suggestion, but I'm not looking for Haskell. It's not what I'm looking for. What I want is declarative, not functional. There is an inherent limitation in the functional approach, I hope to cover why that is in a further article in the series.

I am not after correctness per-se. I am actually more after "cheapness" at least in programmer time. But I do think a lot of the programmer time is spent in things that a solution-describing approach removes, and correctness gets a ride.

Hopefully I am in a right path in that direction!

"but I'm not looking for Haskell. It's not what I'm looking for"

You repeat yourself like this several times in your article, and I find it tedious.

I have often heard Haskell called declarative, it all just depends on how you go about writing your Haskell code. Theoretically Haskell is "time cheap" it just requires more time upfront. That is not to say Haskell is exactly what you are looking for however, I think it is at this point, the closest useful language to what you are looking for.

Are you trying to reinvent prolog? Also, I don't really understand how a compiler for your language would actually figure out the efficient algorithms for getting the answer.

EDIT: I see there's already a bunch of people talking about prolog here. Anyway, the second question is still open :)

I have a feeling the second question will stay open. :)

I believe so too. To choose an efficient algorithm, you have to know things about the input data. Even with the sorting example, this is so; e.g. if you place a certain set of constraints on the input, its possible to sort in linear time. But the compiler has no way of knowing such things, unless, of course, the language has some means of expressing constraints on the input in a manner that is digestible by the compiler...

I don't think this is that hard of a problem. The compiler could have a set of algorithms, each controlled by a set of constraints. Basically the job of the compiler would be to "normalize" a set of constraints such that they can be matched to an equivalent set of constraints from its algorithm toolbox.

From the sorting example, the compiler could recognize that the constraints given match the problem of sorting. If the input data also had the constraint of "integer between 0 and 10,000", it would recognize this as a subset of sorting that could be handled through a linear time algorithm.

The compiler could also be an interpretor. ;) What could be a better way to chose the algorithm than to try them all on the actual data runtime (or in "training mode")?

As an undergraduate, I used a research project at my university that did more-or-less what the author describes.

The system was an "animator" for formal specifications called Possum: http://ww2.cs.mu.oz.au/~tmill/tgf/index.html

Possum would allow you to directly execute a program that was formally defined using the Sum formal specification language. While it was not able to handle every possibility, I found using it to be a really magical experience.

However, in practical terms, the idea of declarative programming has just as many difficulties as ordinary programming: how do you know your specification is correct? how do you debug a logical expression? how do you know your specification matches what you want it to do?

I will look at the project, sounds interesting. If it's like that, I can only

I know declarative doesn't solve the problem of correctness. It's really difficult to define correctness per se! But what such an approach really gains is that you can forget about off-by-one errors, unforeseen cross-conditions in stupid details, so much repetitive code, etc... you will still have the higher-level problems of programming, the efficiency problems, the spec-correctness problems, etc... but nowadays you have those, plus the nitty-gritty details of programming in our paleolitic languages!

I know there are a few initiatives in this area, I really want to have an everyday tool that allows using that kind of approach for everyday problems. It will just make everything so much better for us programmers!

The one_to_one_equal example only works for sets, it looks like. This is a popular example in the Prolog literature, where they say

    sort(A, B) :- permute(A, B), ascending(B).

(permute corresponds to your one_to_one_equal.)

I'm curious about how a compiler can infer the algorithm for sorting. I've played with machine learning algorithms like neural networks and genetic algorithms which might be able to do some of this, but what other things are out there?

I will cover my approach to that in later posts in the series :)

If I were you, I'd look for a space that is more restricted than general-purpose programming but still rich enough to do nontrivial computation. If you can find interesting invariants that are true of all computations in such a space (but not true of all programs in general), you have a hope of leveraging them to create both a powerful declarative language and an efficient implementation for it. The space of all programs in general is too large for this.

This is why SQL and spreadsheets have been such successes as declarative programming. If you find another such model, that could be a big deal.

Sorting is not a good subject for discussing an advanced/intelligent programming language. Try to solve hard problems which are difficult to solve with current languages.

Declarative programming can be very helpful in domain specific tasks. You start with a set of constraints that the computer can understand, and then the core AI will automatically give you the answer. Perhaps then a lot of common people can start to tell computer to do things for them without writing a single line of code, but they need to talk in the languages that computer can understand.

Have you read Elements of Programming by Alexander Stepanov (he of STL fame) and Paul McJones? They take a similar approach as your examples except instead of declarative generation of code they break things down to very rudimentary mathematical definitions of operations and concepts and then build more complexity by bolting them together. Not terribly different than normal programmatic problem decomposition, but they tend to take it a little lower (or perhaps to a higher level of abstraction).

Two quick things jump out at me: (1) This is TDD, without the implementation part of it. (2) There have to be some halting problem issues in here. It's actual realm of usefulness is constrained somewhere, though I'm not exactly sure where.

That said, I've worked with modeling languages along the lines of GAMS that work in this sort of manner. Define a problem - a set of constraints - equations, inequalities, parameters, and the like - push a button, and out pops a solution. Damn useful.

I think it is possible to write something better then prolog but I dont think we will ever write all programmes this way. Dont get me wrong using declerativ systems to help you is often helpful but I doute we will ever programm everything like this.

Even if we did we would still have many of the same bugs, many bugs we have to day are not details of algorithems the are problems in our own head, you can divine a system the way you want it an still get the wrong answer.

I'm not convinced this is possible for anything but a small subset of programs. Such a compiler reasoning about a Turing-complete program would certainly be 'AI-hard', as it would have to essentially be a programmer itself.

What I'm interested in is making proof assistants easier to use by improving their inference capabilities, so programmers can verify the correctness of their programs without having to put in orders of magnitude more work...

I spent some time using systems that seem to do what you are trying to do. One of those is Specware (http://www.specware.org/). When I used Specware their tutorial had a sorting example just like yours but it seems in their latest tutorial they have a different example. My experience is that that those systems are very hard to use and very limited in their capabilities.

Sounds like a combination between flow-based programming and declarative programming. Perhaps a possible approach would be to write a flow-based programming language with some methods marked as "pure" which statelessly map input to output and others able to be written in a more traditional, imperative, less functional style?

In a flow-based architecture, it seems to me that by design, almost every component in the flow would be testable.

We all want, buddy. Now go implement it :)

Sure! I will try to :) I will do so in public, so that I can get as much help as I can.

I'll help what I can. I had a very similar idea, sparked by a conversation in college with a fellow CS major. He was saying how much he liked to program and I said that I hate it. My reasoning was exactly the same as yours, but perhaps broader.

I'd like it if we could get to the point where you say very plainly what you want in your native language (English for me), and then that is interpreted and perhaps more questions are asked by the program until it can implement what you meant. Obviously the problem of NLP is a massive one that will likely never have a perfect solution. There are also the problems of logical inference (if you think this is easy, look up the CyC project). I don't think we should let the current constraints of technology hold us back from designing something better, however.

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

Isn't this just Prolog?

OP here. It's not just Prolog, but indeed Prolog is the closest thing now.

How is it not just prolog?

At the very least, a constraint programming language would be a good basis to start with here.

http://en.wikipedia.org/wiki/Constraint_programming

Specifically, a Prolog-like syntax is also hugely popular in this fascinating Constraint Programming niche: http://en.wikipedia.org/wiki/Answer_set_programming

I don't think there's any existing programming language that does what OP wants.

But Prolog is far from the last word on the subject. For one, it is basically untyped. There are dependently-typed programming languages that can express non-trivial properties via types, which the compiler can check (see ezyang's example).