otini @otini@functional.cafe

Hi everyone! I'm new here so, time for an #introduction?

I'm an M2 student living near Paris, interested in :
• Type systems (Curry-Howard ❤ )
• #CategoryTheory
• #Nix
• #metaprogramming

Today I program a lot in #OCaml, because French research teams use it a lot, but I also use #Haskell and I like dependently-typed languages like #Agda.

For some work I have done on the OCaml compiler you can check out http://otini.chnik.fr/.

Glad to be here :)

Currently worrying of being badly judged for not working on my PhD during summer school and holiday.

Lecture by Magnus Myreen: a fast and verified interactive theorem prover

Very cool!

Just arrived at the Marktoberdorf Summer School in Germany. :) #Marktoberdorf19

I'm going to a summer school and there will probably be stuff to install, and I'm afraid already #NixOS

There isn't even a entry for the newer `nix` command in the Nix documentation, seriously this documentation problem is way worse than I thought

This is one of these days where I regret having installed NixOS on my work laptop.

#NixOS question: trying to install Wolfram Engine from the script/archive downloadable from their website, this is not going well. Is there any way to have '/bin/bash', but also '/bin/rm', etc. to exist and be usable by the script? Yes, I know they shouldn't be using these hardcoded paths.

Reading a journal paper, my supervisor is cited in it. It's normal but it feels weird ^^

Wondering why many people denote \( σ_{\dashv} \) the last element of the sequence σ. Is it because \( \dashv \) looks a bit like −1? 😄

Thunderbird segfaulting, probably yet another Nix-related environment issue that I have no idea how to fix, yayyyyy