Hello everyone! I'm Pablo, a first-year French PhD student based in Paris. I have a background in theoretical comp-sci, more specifically in logic, proof theory, and programming language theory. I'm doing my thesis under the supervision of Benjamin Werner, who already introduced himself in this channel yesterday :) I have been following the FoC podcasts and weekly newsletter for almost two years, and always found the discussions and findings of the community very enlightening and motivating. There is such a feeling of validation when you discover that there is a whole community of like-minded people, who share similar vision and core values in the way they dream about the future of computing ^^ My long-term ambition is to help bringing together centuries of deep philosophical and mathematical knowledge about logic, and decades of experimentations and insights in the design of ergonomic human-computer interfaces. The ultimate goal being to build a solid foundation for a renewed science of programming, that focuses more on the human and social aspects of systems building. Yes, I might be too big of a dreamer, even for the FoC community 😅 To conclude this lengthy introduction on a more concrete note: we are currently working with Benjamin and collaborators on the design of a new kind of graphical interface for proof assistants, based on the direct manipulation of mathematical objects and formulas. We may soon be able to share a very early version of our web-based prototype. We will then be eager to get feedback and insights from the FoC community! As a little teaser, I recently discovered that there may be a formal Curry-Howard correspondence between our work, and the one of Conal Elliott on tangible functional programming... Stay tuned for more info!

Hi! And bienvenue! Good to see more people from France coming here (I am from Toulouse). 😄

Bonjour Nicolas! Nice to meet you 🙂 And what a coincidence, I also am from Toulouse 😲 (lived there for 7 years)

Bring it!

Sounds awesome! Bring on the future of formal proof assistants!

Great to see two of my neighbours join this space! I work at Synchrotron SOLEIL in normal times, just a few km from Lix.

@Konrad Hinsen As they say, it's a small world!

Welcome! I live in Switzerland, so that's like 1/3 French as well. Better proof editors/assistants would be great, my brief stint working with TLA+ had me pretty confused.

@Florian Cäsar I haven't tried TLA+, but it seems to be geared towards verification of imperative programs, whereas our approach targets more general-purpose proof assistants like Coq, Isabelle, Agda... But some interaction techniques might be transferrable to this setting as well!