Week 45 - 2021
The weeknote for 11/8 - 11/14.
Tech
Lean prover
-
Started learning Lean prover. Lean is a programming language and also a theorem prover from Microsoft Research. It can be used as an ordinary programming language like Rust, Golang, OCaml, but also has an ability to prove mathematical theorems. I'm more interested in the aspect of mathematical theorem prover of it.
I ultimately would like to develop my own theorem prover in the future, but it doesn't seem feasible for now because of too much complexity. So I wanted to learn some existing provers first and was looking for 'the best one' to learn for a long time. The first candidate was HOL Light because it formalizes the most items in the 100 theorems, and also the formalized theorems look presented in really clean format. But I found it disappointing after a while because it's not ported to any platform other than some of linux. It also can't build with the latest version of OCaml. It didn't look well maintained. And then I found Lean. It's ported to all major platforms(!), and it even self hosts the compiler(!). So the effort into it looks enormous. The presentation of the theorems are not perfect in my view. Especially the use of non ascii symbols of built-in operators seems terrible to me. I've never seen a language with non-ascii operators got popular. I personally think that's the wrong design, but anyway the runtime works smoothly on my mac. So I decided to learn it for a while.
gpg-agent
- I suddenly was unable to commit anything with git on Tuesday because of gpg signing error. I couldn't figure out the reason of it because the gpg software only reported like 'failed to sign the data' and it didn't provide any further information about the reason of failure. After some research I accidentally fixed the problem with the command
gpgconf --kill gpg-agent. The command was part of the steps of fixing another problem about gpg (I forgot what the problem was). So I finally couldn't figure out the reason, but found a solution apparently.
cdktf
-
I found HashiCorp is now building alternative language interfaces for terraform. It's called CDK for Terraform (or CDKTF).
When I shared it on twitter, it had a lot of attention.
へー terraform が typescript で書けるやつが始まってるのか・・・ https://t.co/tuSrDvWktp
— Yoshiya Hinosawa (@kt3k) November 9, 2021
Life
Baby
-
Our baby is now in the 31th week.
31w🥰 pic.twitter.com/D3HTEfgNH6
— あずき 31w🐘🦕🦖 (@okomekirai) November 11, 2021