My Projects for 2020

This year 2019 has been exciting in many respects, but it’s coming to an end and the time is ripe to look forward: 2020, here I come! For my own personal records, I have written up a list of things I would like to work on, investigate, learn, discover and more generally spend some time tinkering with. I look forward to the 31st of December, 2020, to check by which margin I overestimated the time I could reasonably put into side projects!

Idris

I fell in love with Idris (1) while reviewing Edwin Brady’s awesome book. Having concrete examples of code that leveraged Dependent Types was an eye opener to me. Since then, I have tried to get a better understanding of how dependent types could be put to use in my “Real World”, ie. to improve the design of mundane software.

In 2020, I plan to continue investigating that topic through various angles.

Type Systems and Domain-Driven Design

• How can we use Dependent types and Dependently Typed languages to better model the domains our code works on?
• What are other interesting type systems that could be used for that purpose?
• Homotopy Type Theory looks both extremely fun, extremely abstract and extremely complex for someone who, like me, does not have a PhD in Algebra ; something like a Category Theory but even more hype! Cubical Type Theory is an implementation of HoTT, could it useful to model the kind of problems I encounter in my day job like Double-entry Ledger, payroll software, distributed systems…?
• Two years ago I built an implementation of MiniTT in order to deepen my understanding of such type systems, but this language was too minimalist to be really usable. I have tried again following David Christiansen’s Normalization by Evaluation tutorial, this time in Idris.

IDE and Developer’s Experience

• I have started contributed to the best of my abilities to Idris2 and one area I am particularly interested in is how to improve the developer’s experience, how to leverage the compiler’s machinery to let the developer dialog with the typechecker while building the software?
• Smalltalk was one of the first languages to provide superior tools for development, with an integrated development environment where one could inspect every aspect of the system and dynamically change it, getting instant feedback. Could we do the same with Idris2, letting the developers interact with the compiler and the live system’s state while building it? Idris, like Coq, provides sophisticated tooling for theorem proving which is just the activity of deriving code (proof) from types (propositions).
• Hazel is an example of a system that provides tooling around holes, allowing the developer to build the system partially, providing placeholders (stubs) in areas which need further development while still allowing the system to execute the implemented parts. Surely, there’s something to learn here and implement for Idris!
• Being a practitioner and strong proponent of Pair and Mob Programming, I wish our tools did not suck that much when it comes to sharing with fellow developers! I would like to spend some time building a Distributed Development Environment based on something like Idris to let 2 or more developers collaborate in real time on the development of a system.

Online Games

• I have implemented most of the rules of a wargame in Idris (1 and 2), but have been stuck with turning this kernel into a usable software. I would like to build a UI in Elm that would allow multiple users and multiple simultaneous games, but the support for multi-threading is somewhat lacking in both versions of Idris.
• I had hopes I could leverage Idris2’s underlying Scheme runtime to provide the heavylifting for concurrent channels but unfortunately, the game does not even run on Idris2, probably because of the lack of optimisation in various low-level numeric operations on Nats.
• This lead me to the conclusion that having an optimised low-level backend for Idris2 would be useful. LLVM is the way to go for such an endeavour!

Testing

Property- and Model-Based Testing

• QuickCheck (along with similar packages for languages other than Haskell) is a fantastic tool when our types come short of providing us the necessary confidence in our implementation. My former colleague Stevan Andjelkovic has created quickcheck-state-machines which provides a great implementation of state-machine based testing, allowing one to generate tests from a more abstract automata-like model of a software.
• An idea that is dear to my heart and which I have awkwardly promoted as Homomorphic Event Sourcing is that a single Input/Output State Machine based model could be used both as a tester and as a mock, providing an executable specification to securely develop clients and servers in parallel.
• But once we have FSM models, why not bite the bullet and turn those into proper types, like Session types?
• I definitely want to keep investigating that field, possibly building on QSM package to provide better mocking

FitNesse & ATDD/BDD

• FitNesse has been my favorite BDD/ATDD tool for years, but I must admit it is definitely showing signs of its age: Running a shared instance is somewhat painful to maintain, Wiki syntax is “non-standard” (not there is such a thing as standard Wiki syntax but still…), user experience is terrible when compared to things like http://notion.so … Maybe the time is ripe for starting afresh and create a more modern version of it?
• What if we could combine models, examples, documentation and tests execution within a single tool? This idea is related to the developers experience I have already mentioned, and hints at tools like Jupyter notebooks and Bret Victor’s Ladder of Abstraction
• Maybe the Wiki idea is not so much a useful tool than a barrier to entry for newcomers, esp. non-developers who might be reluctant to code the formatting of a page when they are used to rich UIs? FitNesse is an evolution of FIT which initially interpreted spreadsheets. Given the ubiquity of online spreadsheet tools, I think getting back to a simple tool for interpreting and executing spreadsheets would be worth a try.

Various Software-related stuff

• With Frédéric Merizen I have given in November a trial session of a Functional Architecture course inspired by Michael Sperber and Nicole Rauch own course in German. We plan to build on that experience to provide a commercial version of that training, possibly in several cities in France.
• Having worked for almost 3 years at Symbiont on building a so-called Smart Contracts platform, and more precisely a distributed and decentralised application to manage loans on top of this platform, gave me a new perspective on the potential of Blockchain (aka. Distributed Ledger Technology) for developing distributed systems. I believe a generalised Event Sourcing approach as exemplified in the One Log talk we gave with Yann Schwarz at Codemesh and NCrafts Bordeaux in 2018, is a great way to design and build software system on such platforms.
• I would like to explore how public and/or open-source “blockchain” platforms can support large and complex decentralised applications dedicated to some specific domains like finance, supply chain or even e-government.
• At the theoretical level, I definitely need to improve my knowledge of fundamental principles of decentralised systems, how to model them, how to reason about them, how to verify them… I wonder if Asynchronous automata could not provided some interesting foundations for reasoning about such kind of systems.

Non-software

• Since I have read Merleau-Ponty’s Phénoménologie de la perception, I have been fascinated by Phenomenology: What is it, how does it “work”, what insights does it provide… I have started reading Husserl’s Idées directrices pour une phénoménologie pure et une philosophie phénoménologique in the hope to gather some insights on things like epoché or the phenomenological reduction process.
• I think such tools could be useful as a way to approach software differently, maybe complementing the therapeutical approach I advocated a couple years ago: Analysing software systems as pure phenomena, in the way they appear to the people that work on them or with them, removing the cruft of judgment, prejudices and builtin assumptions about them ; tracking the intentionality behind the relations we have with software intensive systems.
• I recently read Robin K. Hill’s What an algorithm is? and this looks like the kind of analysis I am trying to develop.
• I have also started reading Piketty’s Capitalisme et idéologie which is a “Sequel” to his extraordinary successful Le capital au XXIème siècle. Piketty is one of the few modern-day thinkers that are both optimistic and realistic, providing concrete and actionable - even if counter-intuitive or controversial - solutions to make a better world.
• In the same vein, I recently discovered the existence of Modern Monetary Theory which seems to be a form of Neo-Keynesianism, an heterodox macroeconomic theory that strives to counter neo-liberalist economic theory and restrictive monetary policies that are the heart of our world’s growing inequalities. I look forward to read the book Macroeconomics and form a better understanding of what MMT is and how to rebuild a credible Left alternative.

Conclusion

That’s obviously a ridiculously too high number of complex topics for a single person, in a single year. Especially taking into account I also plan to earn some money with a day job that might not fit perfectly with any of those projects, spend more time with my family, read books just for the pleasure of reading books, run and workout… Let’s see what 2020 has to offer, I will be happy if I can make some decent progress on one or two of those topics!