Dana Scott was awarded the ACM Turing award in 1976 for laying the foundations of the modern approach to the semantics of programming languages.

What is your opinion on the future of software verification?

DS: “We need automation of proofs, but, at the moment, there are no easy-to-use proof assistants. People in Cambridge and INRIA have made very big proofs using proof assistants, but we have to make it more congenial to use for nonexperts. Another problem is that you don’t see the proof when you have finished it: there should be a way to get a printable and readable proof tree out of a formal proof. In this area I can also recommend Robert Harper’s book Practical Foundations for Programming Languages. He is of the opinion that a strong type discipline makes verification easier, and I agree with this.”

What do you think are the most important aspects of good design for programming languages? Can you give some hints on programming language design, in a spirit similar Tony Hoare’s?

DS: “Agree with Hoare’s general principles. Too many languages have been designed for special purposes and then been used as general purpose languages. For example, Java was invented for a special purpose, controlling refrigerators, and then it became a general purpose language. I was hoping for a new version of standard ML, but people couldn’t agree. Pascal has been rather successful, but it has a different evaluation philosophy. Most features needed for a good language already exist, but we need a new synthesis.”

What is your opinion on David Turner’s idea that programming languages should be total? Do we need non-terminating computations?

DS: “I think we do need them, but I don’t do much programming myself. I suggest you ask Robert Harper, Adam Brooks Webber, or Benjamin Pierce.”