Typed λ-calculus for Dummies en

This is a Hands On Lab with limited capacity.

While Functional Programming languages, FP idioms and concepts have become commonplace in many mainstream languages. But do you know the principles behind these concepts, and what makes those principles so appealing and useful? This workshop is a hopefully fun hand-on exploration on the implementation of a simple typed λ-calculus.
Attendees will interact with a program that will guide them to implement, in any language, an increasingly complex typed λ-calculus represented as S-expressions. The presenter will help them through the experiment and clarify concepts.

Against (Formal) Method? en

Formal methods are very often touted as a necessary evolution of software development to cope with increasing complexity, risks, and challenges. After all, if software engineers really want to be considered as “true” engineers like mechanical or nuclear engineers, they will need to embrace formalisation and root their practices and tools in solid mathematical foundations.
But while Formal Methods are probably helpful to answer the question "are we building our software right?", it's unclear whether or not they can answer the equally important question "are we building the right software?".
This presentation puts formal methods (FM) in perspective within the broader domain of software development, as yet another tool to deliver value. Based on the presenter's experience, and some epistemological musings, we shall identify various shortcomings and issues of FM in the software development lifecycle, and suggest ways to mitigate those issues in order to help teams benefit the most from FM, to build the right software in the right way.

Test and Type-Driven Design en

Test-Driven Design (or Development) is a well-known technique that uses "examples" to let the design of a piece of software emerge from the gradual refinement of features, providing evidence of the correct behaviour of the code through the execution of tests.

TDD is great, but, from a modelling perspective, it makes it hard to see the "big picture", to express properties of our domain elements in both a human-readable and machine-checkable form.

Modern type systems as exemplified in functional programming languages like Haskell, Elm, or Idris, are powerful tools to help design and model complex domains: A type can be more than a name or structure definition, it can embed properties of parts of a domain, in order to make impossible states unrepresentable.

The goal of this lab is to introduce the audience to some principles of Type-Driven Development, using features provided by functional programming languages like Haskell and Idris. After a short introduction to algebraic structures and dependent types, we will work on a small but interesting enough domain to model it using a few techniques and tools made possible by "advanced" type systems, hopefully improving both the robustness and the expressiveness of the code.

Designing with QuickCheck Models en

QuickCheck is well-known as a framework for Property-Based Testing whereby one writes tests as properties some code should respect and use generators and shrinkers to prove or find counterexamples to those properties. Building on those principles, quickcheck-dynamic is a tool to define State-Machine like models of software, generate and run sequence of actions, and express properties of the system in terms of high-level Dynamic Logic expressions.
This session is both an introduction to, and an experience report on, the use of quickcheck-dynamic and more generally to the principles and practices of Model-Based Testing. Through a few examples drawn from real-life use of the library, I hope to convince the audience of the relevance of these tools for the development of complex, stateful software.

An Experiment in Phenomenology of code en fr

What if we did not take anything we think we know about the domain, the people, the organisation for which we are building software for granted? If we turned our attention to and focused on how these things appear to us, rather than assuming they are objects external to our consciousness? Would it help us produce "better" software in some sense?
This is a question that Phenomenology, a philosophical approach founded by Edmund Husserl in the early XXth century, attempts to answer within various quarters of human experience.
This talk is an invitation to apply phenomenological investigation tools and concepts like epoché or reduction to code and coding, and observe what is left of things as obvious as domains, users, stakeholders, experts, or even code itself, when we forego assumptions of their objective existence.

While the title of this session sounds pretentious, phenomenology being a complicated word buried under decades of complex writings, I will try to avoid the jargon and anchor it into the day-to-day experience of people actually working with code.
The purpose of this session is to provoke, awaken, puzzle participants and encourage them, or us, to step aside and really think about the things we don't question anymore.

Tentative de phénoménologie du code en fr

Son fondateur Edmund Husserl décrit la phénoménologie comme "la science de l'évidence", soit l'analyse de la subjectivité en suspendant toute hypothèse sur le monde, l'immersion dans la conscience de soi, du monde et des autres. Cette approche a-t'elle quelque chose de nouveau à nous apprendre sur le code et notre rapport à celui-ci ?
C'est à cette question que nous essaierons de répondre dans cette session, explorant l'utilisation des concepts et outils propres à la phénoménologie - époché et réduction, intentionnalité, horizon du monde, flux de conscience... - dans le cadre du code et de la programmation, de l'expérience subjective de ce que c'est qu'écrire, manipuler, interagir avec du code.

Taming the Effects Zoo en

It's 2020 and you've decided it's time to embrace Functional Programming paradigm. You learn Scala or, even better, Haskell, and there starts a long, tiresome and desperating journey through the delightful and frightening intricacies of pure functional idioms, daunting libraries, innumerable compiler extensions and religious wars over semantics of
categorical constructs on social media, to answer THE question: How are you supposed to do something useful with a _pure_ functional programming language, eg. a language that explicitly _forbids_ side-effects?

This talk attempts to answer this question in a somewhat accessible way, by explaining the various ways one can _encode_ side-effects in a pure functional setting. Using a simple but realistic example application, we explore various constructs, trying to assess their relative merits and flaws. Explaining _in concreto_ what are IO monad, monad transformers, free monads, effects handlers and more, should led you to a better understanding of the tradeoffs involved and possibly enlightenment on the real value and power of functional
programming languages.

TDD et TDD sont dans un bateau fr

Le Test-Driven Development ou TDD est une pratique essentielle pour faire croître du logiciel de manière incrémentale et sûre. Mais le mot "Test" dans TDD est trompeur : il n'est pas tant question de tester que de guider le développement en définissant des micro-objectifs, des exemples, automatiquement vérifiés.

Si les exemples sont nécessaires pour comprendre un problème, ils présentent quelques inconvénients :

* leur énumération est quelque peu fastidieuse, répétitive, verbeuse et parfois difficile à relier au problème que l'on cherche à résoudre ;
* ils ne sont pas suffisants pour s'assurer que la solution produite est robuste.

Cette session se veut une introduction à différentes autres approches pour guider le développement :

* utiliser un système de types plus précis pour "rendre les états impossibles non représentables" afin de réduire l'espace à explorer (donc à tester) ;
* définir des propriétés automatiquement vérifiées, ie. le Property-Based Testing, pour guider le développement et accroître la confiance dans le code produit ;
* utiliser des mutations pour prendre en défaut du code "naïf" et améliorer sa résilience.

Je présente ces différentes pratiques en codant en direct un exemple tiré de notre vie quotidienne, la validation d'un numéro de sécurité sociale.

Lessons learnt building a Hydra DApp en

Building Decentralised Applications (DApps), on top of blockchain technology in general, and Cardano in particular, is well-known to be non-trivial. The specificities of the Cardano blockchain and its programming model makes it even more challenging especially as the chain's constraints limit what kind of validations can be done on-chain.
Hydra Head aims to provide a way to scale Cardano notably by allowing DApp builders to overcome those limitations.
This talk will be an experience report building a DApp leveraging Hydra to allow playing Chess.

* This is a talk based on the code available at https://github.com/abailly/black-jack
* It's meant to highlight what can and cannot be done, from my personal experience, and provide advices to wannabe DApp developers on how to approach this problem