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.
example, my view may be very limited, but I see academic research
getting into completely different directions than software engineering
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
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.
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.