I couldn't agree more that programming is an art. But mathematics is also an art and programming is an art only insofar as it borrows important aspects from the field of mathematics. There is certainly a good deal of creativity involved in programming, but the bulk of the creativity is in devising novel, elegant and efficient algorithms, not in representing them using some particular programming language which it typically takes just a matter of weeks to pick up.
The analogy used by the student is an important one. But we should ask the question: Where is the "art" in painting? Is it in learning to weild the brush or is it in the creative expression of the painter? Most people would agree when I say it is in the latter.
The correct way of looking at the analogy would be to compare learning to weild the brush with learning a particular programming language and the artistic abilities with the mathematical and logical skills of the programmer. In other words, coding is the skill and algorithm design is the art.
Programmers who think that mathematical skills are unnecessary for their jobs are at best deluding themselves into taking the easy way out, just as painters would be deluding themselves if they believed they could come up with a piece as good as Picasso's by just learning how to weild a brush properly.
If I had to employ programmers and I had two applicants to choose from and only one of them was mathematically adept, my choice for the mathematically inclined would be straightforward and simple. Fortunately for the non-mathematically inclined among today's programmers, there is a severe shortage of skilled people in the coding arena, and so they are easily able to find work under the blanket job-title of programmer.
Remember that the Sistine Chapel is seen as the work of Michaelangelo, although he probably had little to do with the actual painting of it. We know today that he had several skilled painters in his employ who were responsible for giving form to his artistic conceptions. The real artist is Michaelangelo.
As I thought about this, I came up with a revised answer to the question which I hope will be more satisfactory. One could perhaps imagine three major kinds of errors that can happen in a program -- syntax errors, typographical errors, and logic errors. I would tend to group errors in translation of algorithm into code along with the former two kinds. Now, upon recollecting the incidents in the past when I have had a program which I had verified mathematically fail on me, I realised that none of the failures were in fact due to an error of type 3, logic errors. All of them were either syntax or typographical errors such as a missed pointer symbol, errors in translating the algorithm into code or other oversights where some crucial components in the proof had been omitted from the actual implementation. Of course, in large systems, these tend to be fairly difficult to detect and even debugging these takes a while. But the important point is that none of these were actually logic errors.
Syntax errors are easy, any half decent compiler and editor will flag them for you to fix. Typos and omissions are slightly harder, but they will be fixed eventually. The hardest are logical errors, which tend to be practically impossible to identify and fix in large systems. Typically, it is only logical errors in the code and algorithm that we are really concerned about and it is these that our mathematical proofs are concerned with. So my revised answer is
"Yes it is still possible to have a buggy program even after it has been verified mathematically, but these bugs will be due to other kinds of errors than logic errors. The proof only checks out the program for logic errors and these will surely be absent if the program checks out mathematically."
While the surface aspects tend to change, the foundations of CS are still the same as they have always been. If one wants to learn a standard like CORBA or ISO/OSI for instance, one should be prepared to accept the fact that the standard may change, sometimes dramatically, and need to re-learn it. But the foundations of computer science, much like those for any other science tend to be the same, mostly anyway. Indeed, one can safely say that if something in the foundation itself changes, the resultant change in many surface structures such as CORBA or ISO/OSI would so dramatic as to require a complete re-engineering in many cases. We should thus be glad that much of the foundational results are relatively stable.
Of course, it is possible that some newer books use different ways of presenting the information to aid the student in better assimilating it. This could perhaps have resulted from recent research in the psychology of learning. But then again, there is also the trade-off between information content vs presentation. Not all well presented books have the same quality of information in them. And I haven't at this point any evidence that any particular way of presenting the foundation material in CS is better than the traditional way. Nor have I found a book that presents all the material in the prescribed text in a better way. After all, when you go on to do research in the field, you will have to learn to read journal papers and technical articles which are all still presented using traditional techniques. So you might as well get used to it now.
Regarding the latter form of the question, which relates to the language one should use to teach this course, well again, since this is a foundations course, I don't see a need to use any particular programming language, as long as the language we do use is powerful enough and readable enough. In fact, the only reason we don't use Knuth's decades old "The Art of Computer Programming" is because of the relative unreadability of the MIX assembler-like programming language in which most of the algorithms are coded, as compared with say C or Pascal. I don't believe that Java or Visual Basic is any more readable than C, Pascal, or just structured English.
Understanding the fundamentals is more important than learning the programming language. One can always go from the former to the latter easily, but not the other way. As an example, a professional Visual Basic programmer contacted me recently asking for a high-level description of one of my algorithms that could be implementable in VB. The problem was that the algorithm needed to manipulate individual bits in the data and he wasn't sure how to do this using VB's rather limited bit-manipulation capabilities. I knew no VB, but it didn't take long to come up with a version of the algorithm that gave him getBit() and setBit() functions implementable in VB. One can prove by mathematical induction, for instance, that "if the nth bit of a number is 1, then that number should be divisible an odd number of times by 2n. Consequently, one can write bit manipulation algorithms in languages which don't explicitly support this.