I applied to give a theorem proving seminar at a university. They chose Philip Wadler as a lecturer over me. That must have been close! Still, so disappointed…
To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.
Isn’t it ironic – Google’s own proprietary Meet service isn’t supported in Chromium, a web browser by Google, but it is supported in Firefox, a web browser by Google’s competitor.
Jo Freeman has an interesting essay on the tyranny of structurelessness. The lack of structure implies the lack of power to act.
I’m happy to announce that I’ll be speaking at the Lambda Days 2019 conference! I’ll be giving a talk on function totality.
Earlier this week I got a Lego Mindstorms EV3 robotics kit. I was aware there is a Haskell binding, but I didn’t know it is compatible only with the earlier NXT generation of the Mindstorms line, at least according to the Wikipedia page on EV3. I’m hoping to find out today if the NXT Haskell library can nevertheless be used with the EV3. If not, I’m likely to start writing a Haskell library for EV3.
As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.
The upcoming Tuesday I will be giving a talk at the IEEE Croatian Section on function totality. The talk will take place at the University of Zagreb, the Faculty of Electrical Engineering and Computing.