自己紹介

Emacs を日々使っている。日常生活で扱う情報は全てEmacsで管理している。 予定を立て、日記をつけ、睡眠の記録を取り、プログラムを書くといった生活の基盤が全て Emacs を中心に回っている。

また、この「TojoQKの投稿」というサイト自体もEmacsで書いているし、CIサーバーにてEmacsが生成したHTMLをWebサーバーにデプロイしている。

また、この「TojoQKの投稿」というサイトを動かしているサーバーのOSもGuix Systemである。 nginxの設定は全部Guix Systemで書いているし、このWebサーバーはGuixの記述にないことは何もしていない。

この2025年頃からAgdaに深くはまっていて、もはやAgdaが最も好きなプログラミング言語になった。

私にとって Agda の価値とは論理的整合性の保証にある。 わたしはもともと Emacs の org-mode でテキストを用いて全て記述しようと考えていた。 しかし、実際のところただのテキストは危険すぎる。 なぜなら、テキストによる記述というものは他との整合性をそれ単体では何も保証してくれないからである。 だからといって、テキストの利便性を捨ててDBを使ったりということは私のポリシーにあまりにも反していた。

こういった問題は org-mode と Agda を組み合わせて文芸的プログラミングをすることで完璧に解決した。 いままで通りテキストで記録を取るのでよい、しかし Agda で文書を型チェックすることでその記述の論理破綻を防ぐことができる。

この目的に便利に使える仕組みのは私が知る限りでは Agda しかない。

専門的に勉強しているわけではないが関心がある。中学生のときに知った。 集団の平均値だけ見てはずれ値を無視したり人の特性ばかりに注目して状況を無視したりする他の分野と異なり個人にフォーカスして行動の制御に取り組むことができているところに魅力を感じている。

最近触れる機会が減少してしまっているが、好きではある。 Guix System のパッケージ/システム定義に Guile を使っているし、Emacs を制御するのに Emacs Lisp を使っている。

かつては型付き Lisp の Tyepd Racket や Coalton について可能性を大いに感じていたのだが、 そもそも依存型のないプログラミング言語を趣味で使うことがなくなってしまっており、 それゆえ趣味のプログラミングは全て Agda に持っていかれてしまった。 とはいえ、もともとLispで静的なメタプログラミングをしていたからこそ、 Agdaの依存型を受け入れることができたという側面が多分にあると思う。

ユーザーが自分の計算機を自由にコントロールできるのが当然の時代が訪れるように貢献したい。

2020年の7月に Free Software Foundation の Associate Member になった。