I want to fix programming

Sounds like a delightful blend of Agda and Prolog.

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!

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.

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