An short interview with Dana Scott

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum

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.”

Dana Scott
@Klaus-Tschira-Stiftung / Peter Badge

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.”

Avatar photo

is a senior software engineer at Google Zürich, where he has contributed to several public launches and submitted ten patent applications since joining Google in 2011. He studied intuitionistic type theory under Per Martin-Löf, who invented the subject. His PhD thesis is published by Springer under the title "Treatise on Intuitionistic Type Theory". Johan is an active member of the academy: he has published several books and scientific papers; he is a reviewer for Zentralblatt MATH; he has delivered dozens of public lectures; and he is frequently consulted as a referee, both internally at Google and for external conference and journal publications.

Leave a Reply

E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +