Hacker News new | past | comments | ask | show | jobs | submit login

This is brilliant and well explained - I saw where you were headed just before you got there. And had a little clap of delight to see my suspicions were correct.

However, don't you think the reason for the success of Maxwell is because the objects it describes are well behaved and can be completely described by a set of partial differential equations? Where as the constituent atoms (hehe) of software are themselves complex objects - more than just point particles whose state can be completely described by say a wave function. And their behvior effectively solvable by simple deduction from physical postulates and the axioms of mathematics. I believe I saw a story about Feynman deriving a bunch of partial differential equations to predict the behavior of a program. But I do not think such an approach is scalable.

But the core of your idea I believe is that by specifying invariant in some theory which encapsulates the possible evolution of all possible programs then you can write programs far more simply? Essentially the next level of a synthesis of programming with unit tests, data and automatic programming. I believe the main impedance to this (I think) is that any such general evolution function would be incomputable. And where as with Maxwell equations the space is limited and the boundaries defined and embodied and easily deductively traversed, for a program the search space would be massive and difficult to search effectively. In effect, I believe you have just specified an AI complete problem.

Notice also that even a classical theory like general relativity yields few analytic solutions and numerical simulations are expensive. Perhaps this hints at why a unified theory is so difficult to come by? While the constituents are still simple particulates, the size of a theory/program which encompasses in totality all possible behaviors in nature might require a chain of reasoning so deep it lies beyond the ken of unaugmented humans. I believe a unified theory of efficiently searchable programs would be even more difficult - such a theory would yield a unified theory of nature as a special case.




The story you read about Feynman is this one: http://longnow.org/essays/richard-feynman-connection-machine...

I remember seeing a program that would output Haskell functions given just their type signatures. If you think of type signatures as invariants, this is exactly what drostie described. Alas my Google-fu was unable to find a reference to it.


I know that one :D, here I can help: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/d...

I have considered this road, see this LtU discussion to see why this approach though wonderful, is still too limited for general programming. http://lambda-the-ultimate.org/node/1178

Essentially, as is found in many automatic program derivation attempts, recursion explodes complexity.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: