Learning to program is hard! There are so many things to think of: syntax, data structures, problem solving.
What if we could make a programming language that grows with you, and becomes stricter and more complex over time? In this talk Felienne outlines Hedy: her gradual language for programming education, and how it was designed. She will also reflect on what she has learned from trying Hedy with groups of children and from analyzing the first 500.000 Hedy programs.
The last few decades have seen tremendous strides in various technologies for reasoning about programs. However, we believe these technologies will only become ubiquitous if they can be seamlessly integrated within programming so that programmers can use them continuously throughout the software development lifecycle. In this tutorial, we will learn how refinement types offer a path towards integrating verification into existing host languages, by integrating the compositional nature of types with the expressiveness of logics, and the automation of model checking. We will see how refinements allow the programmer to extend specifications using types, to extend the analysis using SMT and abstract interpretation and finally, to extend verification beyond automatically decidable logical fragments, by allowing programmers to interactively write proofs simply as code in the host language.
The tutorial will include hands-on exercises, so be ready with your laptops!