14 ms·
I want to fix programming
- th0ma5 15y agoAs 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.
- andreyf 15y agoSounds like you're talking about genetic programming: https://en.wikipedia.org/wiki/Genetic_programming https://en.wikipedia.org/wiki/Genetic_programming
- judofyr 15y agoIt took the universe 13.7 billion years and an ever-expanding memory space; I'm not entirely sure if this is the right approach…
- MattRogish 15y agoIsn't that just BogoSort? :) http://en.wikipedia.org/wiki/Bogosort http://en.wikipedia.org/wiki/Bogosort
- RodgerTheGreat 15y agoTo 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 http://en.wikipedia.org/wiki/Superoptimization
- jules 15y agoYou 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.
- jholman 15y agoIsn't this just Prolog?
- jng 15y agoOP here. It's not just Prolog, but indeed Prolog is the closest thing now.
- ryanbraganza 15y agoHow 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 http://en.wikipedia.org/wiki/Constraint_programming
- dualogy 15y agoSpecifically, a Prolog-like syntax is also hugely popular in this fascinating Constraint Programming niche: http://en.wikipedia.org/wiki/Answer_set_programming http://en.wikipedia.org/wiki/Answer_set_programming
- nandemo 15y agoI 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). See also: http://stackoverflow.com/questions/2829347/a-question-about-logic-and-the-curry-howard-correspondence http://stackoverflow.com/questions/2829347/a-question-about-...
- ggchappell 15y agoA thought-provoking post. (More detailed thoughts left as a comment on the post itself.)
- nddrylliog 15y agoWe all want, buddy. Now go implement it :)
- jng 15y agoSure! I will try to :) I will do so in public, so that I can get as much help as I can.
- AUmrysh 15y agoI'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.
- Craiggybear 15y agoYup. He's right. The future isn't going to be programming digital machines anyhow. Its going to be programming living matter. But that's another story.
- raganwald 15y agoDear 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.
- ryanbraganza 15y agoTake a look at quickcheck if you want something that works today. http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck http://www.haskell.org/haskellwiki/Introduction_to_QuickChec...
- jng 15y agoReg, 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.
- Peaker 15y agoThe "Why Dependent Types Matter" paper at http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf 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.
- simon_weber 15y agoThis is called declarative programming (http://en.wikipedia.org/wiki/Declarative_programming http://en.wikipedia.org/wiki/Declarative_programming), as opposed to imperative programming.
- jng 15y agoSure, 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.
- simon_weber 15y agoProlog 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.
- MattGrommes 15y agoYou 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. :)
- ben314 15y agoAs 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 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?
- jng 15y agoI 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!
- Ygor 15y agoFor 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 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.
- skizm 15y agoSo 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?
- Tuna-Fish 15y agoDeclarative 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.
- AUmrysh 15y agoFor 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.
- doty 15y agoThis 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.
- batista 15y ago"Programming is broken. Completely broken." What something starts like this it usually translates to: "I don't understand pragmatic hardware/complexity/market etc constaints and engineering compromises".
- jng 15y agoMight be. Hopefully not. I have done a huge amount of programming though, so it's not like the reflection comes from ignorance. Under the mess of spaghetti code that anything out there is now, I see a clean structure of code trying to come out. I want to help it come out to the surface.
- derekp7 15y agoGenerally, what I've found is the reason for the big pile of mess is not that the methodology is wrong, but quite frankly the programmer didn't know what needed to be done until the program was completed. Even with a complete set of requirements, if you are writing anything of any complexity then by definition it hasn't been done before. But you can usually take an existing program, re-define the specification, and re-write the code in a much cleaner and correct fashion (assuming you avoid the temptation to add new features at the same time).
- protomyth 15y agoThe 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.
- espeed 15y agoThe most common declarative programming language used in SQL. Or maybe a spreadsheet (http://philip.greenspun.com/panda/databases-choosing http://philip.greenspun.com/panda/databases-choosing).
- protomyth 15y agoalthough I respect Philip Greenspun greatly, most spreadsheets I have seen are pretty procedural. People tend to think in steps on those types of calculations.
- deleted 15y ago[deleted]
- lubutu 15y agoI'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...
- barrkel 15y agoSo 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.
- jng 15y agoYou 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 :)
- AUmrysh 15y agoI'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?
- jng 15y agoI will cover my approach to that in later posts in the series :)
- mbrubeck 15y agohttp://lukepalmer.wordpress.com/2012/01/19/sentences-and-paradigms/ 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.
- maeon3 15y agoMy vision of the future for programming is a room with 3d virtual reality goggles. Monitors are nowhere to be found, lines of code in files are presented to you on virtual monitors around you in a 760 degree panoramic view, above, below, and THROUGH. Our brains are evolved for a 3d world, not the lines-of-code on printed page world. Commands like "instantiate new object", "add items to object", "do an sql query", "run sql query", "sum the integers", suck. These commands will be represented in 3d space like a flow chart with general directives. When you want to "zoom in" on one of the boxes, you can see the particulars of how it takes place. Zooming out shows you a perfect representation of the general directives, zooming in takes you to the nitty gritty commands, and zooming in further shows you the bits being shifted around on the hardware.
- svdad 15y agothat's actually not that far from what programming with well-designed libraries and abstractions is like now. at least, I know I have a more-or-less 3d visualization of my program in my head as I'm working on it... but that could be just me.
- psykotic 15y ago> 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).
- Gigablah 15y agoI took a course on magnetic storage technology and now I'm perpetually amazed that computers even work.
- dustingetz 15y agoJon, 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.
- jng 15y agoDusting, 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!
- mdonahoe 15y ago"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.
- jimmyjazz14 15y agoI 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.
- apsp 15y agoNot 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]
- ezyang 15y agoHere 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://coq.inria.fr/stdlib/Coq.Sorting.Sorted.html
- andrewcooke 15y agohttp://www.cis.upenn.edu/~bcpierce/sf/ 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.ps.gz http://www.fing.edu.uy/inco/cursos/proggen/Articulos/sorting... (isn't that kinda what you want?)
- aaronblohowiak 15y agoSounds like a delightful blend of Agda and Prolog.
- dxbydt 15y agoI 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!
- iso8859-1 15y agoI 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.
- chegra84 15y ago“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-doesnt-like-coding http://chestergrant.posterous.com/your-favorite-programmer-d...
- jerf 15y agoSo, 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.
- abecedarius 15y agoThe 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.)
- javadyan 15y agoAre 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 :)
- balloot 15y agoI have a feeling the second question will stay open. :)
- javadyan 15y agoI 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...
- hackinthebochs 15y agoI 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.
- bjornsing 15y agoThe 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")?
- gruseom 15y agoIf 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.
- asimeqi 15y agoI spent some time using systems that seem to do what you are trying to do. One of those is Specware (http://www.specware.org/ 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.
- ChristianMarks 15y agoThe 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 http://cfpm.org/pub/papers/tiofdm.pdf I suggest looking at Robert Harper's book on type theory instead.
- rmcclellan 15y agoI 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.
- dullcrisp 15y agoCan 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?
- jng 15y agoYou 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.
- philh 15y agoMy question: what can this not solve? What problems could a human solve that this language couldn't? I think that would help me get a better idea of what you're trying to accomplish.
- DenisM 15y agoThe 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.
- jng 15y agoYes I'm amazed with that too! And really enjoying it myself!
- DannoHung 15y agoYou have to define the way that the sort should work though, and at that point, what you really want is functional dependencies. Coq, Idris, Agda, etc, etc. Not a lot of fun to learn how they work, but they're really quite impressive.
- koko775 15y agoSounds 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.
- DenisM 15y agoYou 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.
- giberson 15y agoSo 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.
- timmaxw 15y agoThere'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.
- giberson 15y agoTongue 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.
- wccrawford 15y agoActually, 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.
- omaranto 15y agoIt 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...
- ComputerGuru 15y agoBullshit. Sorry, but there's nothing essentially "broken" about programming. You don't like it, but it's a model that works. Until you create a true AI, this is the way things are. It's not broken, it's apples and oranges. Instead of fixing programming, fix your way of looking at it.
- ilaksh 15y agoAlso see Mozart/Oz and other constraint programming systems. http://en.wikipedia.org/wiki/Constraint_programming http://en.wikipedia.org/wiki/Constraint_programming
- studentrob 15y agoCame here to say this.. the language already exists!
- balloot 15y agoBest of luck, though this strikes me as a "Everyone should have a pony!" sort of thing. You're basically asking someone to build some magic compiler that handles all the logic AND does so efficiently. It seems if this were possible it would have happened by now.
- bjornsing 15y agoJon, I think you're on the right (or at least an interesting) track here, one that I have been thinking about a bit myself. For me these thoughts came after working for a few years on a clean room reimplementation project for a software component with a large set of automated tests (thousands). Slowly I got the feeling that each of those tests could be seen as an image of an unknown object, and that my job was to construct that object. Looking at just a few pictures it might be easy to find an object that could be projected onto planes to create those images, but looking at thousands of images it can be a very intellectually challenging task to find a single object that matches all of them. It's also a problem that has far more dimensions than the 3D world we live in. In agile programming you may call those images "user stories". Agile basically says "there is no way to know all the images beforehand (because that depends e.g. on a market response), so just start with the most important images and build the simplest possible object that fits with them". Each time you add in a new image there's a risk that you have to make major changes to the object (to make it fit with the new image while remaining "compatible" with the previous images). That's what's called refactoring. The really irritating thing with programming is that the effort of building a program does not scale linearly with the number of images (at least not in most cases). There is really no limit to how much work you may have to do to make the object fit with one or several new images, while remaining compatible with all the previous ones. That's because imperative code is a description of the object and not a description of the images. What a programmer does is really solving the global optimization problem of constructing a minimal object that fits a number of images, and then writing that down in code. The better the programmer the more images they can handle, the more beautifully the images will match the object and the simpler the object will be. It must be possible for a machine to do this. Don't get me wrong; it's a formidable optimization problem - and there are certainly sets of images for which no (reasonable) object can be constructed - but in principle it must be possible. In fact there is a machine that does this for simple x-ray images and physical 3D objects: a Computerized Axial Tomography machine, or CAT scan as they call them in hospitals. Basically, what these machines do is take a series of x-ray images of an unknown object and then compute "backwards" what that object must be like on the inside in order to have created those x-ray images. I bet a really good programmer would be great at manual tomography, and that when you have implemented your new programming paradigm it will be a sort of CAT scan for software. :) I'd love to talk more about this on occasion!
- icebraining 15y agoIsn'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.
- daviddaviddavid 15y agoHere's a Prolog implementation of bubblesort (taken from Bratko's Prolog Programming for AI). bubblesort(List, Sorted) :- swap(List, List1), !, bubblesort(List1, Sorted). swap([X,Y|Rest], [Y,X|Rest) :- gt(X,Y). swap([Z|Rest], [Z|Rest1]) :- swap(Rest, Rest1).
- joe_the_user 15y agoHope 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...
- mhewett 15y agoYou are missing the point. The point is not for everyone to write perfect code in some mythical perfect language. They can't do it and there isn't any such language. The solution is for everyone to re-use the nearly-perfect code we have that is written by the few who can write it.
- bfrs 15y agoRelevant stuff from SICP [1]: "The contrast between [a mathematical] function and [a computing] procedure is a reflection 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 specified 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#%_sec_1.1.7 http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-10.html...
- bjornsing 15y agoYea, 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).
- jowiar 15y agoTwo 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.
- chj 15y agoSorting 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.
- ryanmolden 15y agoHave 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).
- yason 15y agoAs 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.
- jng 15y agoI 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.
- nnq 15y agoWhy 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]
- wladimir 15y agoI 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.
- apl 15y agoHow does that differ from, say, Haskell's QuickCheck [1] and its ten thousand counterparts in other languages? [1] http://en.wikipedia.org/wiki/Quickcheck http://en.wikipedia.org/wiki/Quickcheck
- nnq 15y ago
- Xion 15y agoThe 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?
- jaekwon 15y agodef factor(input) = prime: input % prime = 0 prime > 1 Even worse... def fermat() = a, b, c, n: a^n + b^n = c^n n > 2
- wccrawford 15y agoI'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.
- jng 15y agoI'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.
- nickik 15y agoI 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.
- bad_alloc 15y agoI 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.
- jng 15y agoProgramming 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!
- obiefernandez 15y agoThe thought reminds me a bit of what Charles Simoniy has been trying to do for years with Intentional Software
- jng 15y agoI know about that initiative! I think it points in the right direction. I think the approach they took based on DSLs and editors is what doesn't work.