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!
Facebook's main website, ads platform, and much of its internal tooling is implemented in Hack, a language that evolved from PHP by removing the worst features and by adding static typing and modern constructs for asynchronous programming. Its type system is an interesting mixture of ideas from Java, C#, Scala, and OCaml, with flow-sensitive typing thrown in to capture typical PHP idioms and a few unique features. These days developers demand ever richer types, and evolution of the codebase goes hand-in-hand with evolution of the type system and programming language. In this lecture I will review some features recently added to Hack, highlighting the unique entanglement between developer needs, language design challenges, and practical implementation constraints.