Niki Vazou Lambda Days 2017 Interview

Niki Vazou will be giving a talk at Lambda Days 2017. She will be speaking about Liquid Haskell.

Follow Niki on her Homepage, GitHub and Twitter.

PurelyFunctional.tv: How did you get into Functional Programming?

Niki Vazou: I was really glad to get introduced to functional programming (and in fact Haskell) from my introduction to computer science, first semester course in my undergraduate studies in National Technical University of Athens. This was my first time I had to program and I could choose to program in a functional language! I loved it from the first time because I came from a math background and functional programming was just putting maths into action

PF.tv: What is your talk about?

NV: In my talk I present Liquid Haskell and how one can use it to turn Haskell into a theorem prover. Liquid Haskell decorates Haskell types with logical predicates and uses SMT to check proterties of your program, ranging from in bounds indexing to associativity of the list append function.

PF.tv: Who is your talk for?

NV: Anyone who is interested in functional programming and logic and cares to produce safe code. No previous knowledge is required though I do use Haskell syntax in my examples that may initially confuse people totally unfamiliar with Haskell.

PF.tv: What do you hope people will take away from the talk?

NV: I hope that people who will attend my talk will get persuated that we can take advantage of sophisticated formal method techniques and the state of the art SMT solvers to create useful and usable program verifiers, like Liquid Haskell.

PF.tv: What concepts do you recommend people be familiar with to maximize their experience with the talk?

NV: The concepts I touch in my talk are type systems, theorem proving and SMT solvers. If attendees are familiar with these concepts they will be able to understand exactly how Liquid Haskell works internally. Though, the goal of my talk is to present how one can use Liquid Haskell without knowing exactly the techinical details of verification.

PF.tv: What resources are available for people who want to study up before the talk? Are there any projects you'd like people to be aware of? How can people help out?

NV: You can find more about Liquid Haskell in - our website : https://ucsd-progsys.github.io/liquidhaskell-blog/ - tutorial: http://ucsd-progsys.github.io/lh-workshop/ - trying it online: http://goto.ucsd.edu:8090/index.html - installing it locally: cabal install liquidhaskell - github repo: https://github.com/ucsd-progsys/liquidhaskell

People can help out by addressing our existing github issues or their newly found bugs in pull requests!

PF.tv: Where can people follow you online?

NV: My website: https://nikivazou.github.io/ My tweeter: https://twitter.com/nikivazou

PF.tv: Where do you see the state of functional programming in 10 years?

NV: The past few years the number of companies that use functional programming in everyday, real-world, industrial applications have been significantly increased. This increase happened due to the advantages of strong typing and controlled side effects that allow for self-documented code, programs that rarely crash and easier parallelization. In the next 10 years I expect the industrial users of functional programming to keep growing.

What I really would like to see though is functional programming languages to be used to introduce (even high school) students into programming. I trust that in 10 years this can happen!

PF.tv: If functional programming were a superhero, what superpower would it have?

NV: Healing ability (via types!)