Tue, 13 Jul 2010 21:57:30 GMT
Finally, my project thesis is over. Over. Woooohoo! Now I can proceed with trying to get my diploma.
Well, the topic was strongly connected to program extraction from proofs. Which is a topic hardly in-between mathematics and computer science. One the one hand, it produces algorithms which can be verified from mathematical proofs, which makes it interesting for computer science. On the other hand, these proofs mainly have to be constructive, which gives interesting applications to constructive mathematics.
Both topics are rather niche-topics of both sciences, I didnt quite understand why, until now that I have prepared my report on that topic, which should show it to people not familiar with it. I thought the topic itself was rather trivial and the main efforts are taken in finding clever relations to increase the usability, but in fact, there is a lot of things to know and a lot of intuition to gain, until one can really work with it and see the beauty of all of it.
Which will probably never be done by "professional" programmers. It takes too long to explain the advantages, and its not "cheaper" to use, "beauty" is not interesting in IT.
Whats the future of programming? A question I often wonder about.
For example, my view may be very limited, but I see academic research getting into completely different directions than software engineering does.
One thing that one has to accept (I guess) is that there is no future for Lisp and its dialects as a language of wide-spread use. Scheme seems to me not to be a good choice for portable programming of large systems, and Common Lisp is too anachronistic in some senses, and still too "innovative" for the ordinary programmer which currently learns to accept some circumsized version of lambda-abstractions in C/C++.
Still, Lisps are good languages for doing research stuff, and I dont think that they will vanish. I think they will stay being what I think they are now: A niche for people who dont want to wait another century until its concepts finally find their way into the mainstream. I see program extraction from proofs having its future in the lisp-world, because it fits more into it than into others. You may have a type-system which is similar to functional languages rather than lisp, but the essential parts are the proofs which produce the algorithms - the program. Which is whats central to lisp rather than functional programming languages.
Then there are a lot of languages that are basically made for the laziness of people, exchanging programming complexity by computer power. I think of PHP and several other scripting languages. There is nothing wrong with this, as long as it stays small, but I am afraid it wont. I assume there will come a lot of fancy new such languages which basically do subsets of the stuff Common Lisp does (as they do today) but in a worse and slow way.
Since functional programming is so hardly pushed in universities, and direct formal program verification, i.e. not extracting the program from a proof but proving the correctness of a program, is something that is basically a lot easier under functional langugages, I think there will soon or later be some mainstream-language, and I am afraid Haskell will be this language. It has everything a hype needs: A lot of weird stuff only people who are really willing to get deeply into it can understand but still not being too complicated for an ordinary undergraduate student, a lot of special cases, especially in its syntax, with which people can do things in a way they can act up with their superior knowledge.
In the end, it will stay chaotic. As it is now. But in the end, its just programming. Who cares.
Well, the topic was strongly connected to program extraction from proofs. Which is a topic hardly in-between mathematics and computer science. One the one hand, it produces algorithms which can be verified from mathematical proofs, which makes it interesting for computer science. On the other hand, these proofs mainly have to be constructive, which gives interesting applications to constructive mathematics.
Both topics are rather niche-topics of both sciences, I didnt quite understand why, until now that I have prepared my report on that topic, which should show it to people not familiar with it. I thought the topic itself was rather trivial and the main efforts are taken in finding clever relations to increase the usability, but in fact, there is a lot of things to know and a lot of intuition to gain, until one can really work with it and see the beauty of all of it.
Which will probably never be done by "professional" programmers. It takes too long to explain the advantages, and its not "cheaper" to use, "beauty" is not interesting in IT.
Whats the future of programming? A question I often wonder about.
For example, my view may be very limited, but I see academic research getting into completely different directions than software engineering does.
One thing that one has to accept (I guess) is that there is no future for Lisp and its dialects as a language of wide-spread use. Scheme seems to me not to be a good choice for portable programming of large systems, and Common Lisp is too anachronistic in some senses, and still too "innovative" for the ordinary programmer which currently learns to accept some circumsized version of lambda-abstractions in C/C++.
Still, Lisps are good languages for doing research stuff, and I dont think that they will vanish. I think they will stay being what I think they are now: A niche for people who dont want to wait another century until its concepts finally find their way into the mainstream. I see program extraction from proofs having its future in the lisp-world, because it fits more into it than into others. You may have a type-system which is similar to functional languages rather than lisp, but the essential parts are the proofs which produce the algorithms - the program. Which is whats central to lisp rather than functional programming languages.
Then there are a lot of languages that are basically made for the laziness of people, exchanging programming complexity by computer power. I think of PHP and several other scripting languages. There is nothing wrong with this, as long as it stays small, but I am afraid it wont. I assume there will come a lot of fancy new such languages which basically do subsets of the stuff Common Lisp does (as they do today) but in a worse and slow way.
Since functional programming is so hardly pushed in universities, and direct formal program verification, i.e. not extracting the program from a proof but proving the correctness of a program, is something that is basically a lot easier under functional langugages, I think there will soon or later be some mainstream-language, and I am afraid Haskell will be this language. It has everything a hype needs: A lot of weird stuff only people who are really willing to get deeply into it can understand but still not being too complicated for an ordinary undergraduate student, a lot of special cases, especially in its syntax, with which people can do things in a way they can act up with their superior knowledge.
In the end, it will stay chaotic. As it is now. But in the end, its just programming. Who cares.