aboutsummaryrefslogtreecommitdiff
path: root/posts/about-me.md
blob: cb8c60adadfda3c65dcbd90678fa37e3e6d7e164 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
title: About me
id: about-me
date: 2020-02-19 00:00
updated: 2021-09-12 12:00
description: 自己紹介ページ
---

## 自己紹介



### 自由ソフトウェア

[自由ソフトウェア](https://www.gnu.org/philosophy/free-sw.ja.html)が好きでユーザーが自分の環境で動かすプログラムをコントロールできるのが当然の時代が訪れる未来のために貢献していきたいと考えています。

2020 年の 7 月から Free Software Foundation の Associate Member を続けています。

[![FSF の Member
button](https://static.fsf.org/nosvn/associate/crm/5002583.png)](https://my.fsf.org/join?referrer=5002583)

FSF は自由ソフトウェア普及させるための活動を精力的に行なっています。あなたも一緒に [FSF
を支援](https://my.fsf.org/join?referrer=5002583)しましょう。



### ACL2 による定理証明

ACL2 は定理証明支援系の一つで、Common Lisp のサブセットでもあります。最近はこの ACL2
を使って定理証明をするのにはまっています。初見では自分が使えるようになる気がまったくしなかったのですが、ちゃんと勉強すると意外に使えるようになるので結構おすすめです。

ACL2 を使って書いた定理を
[acl2-theorems](https://git.tojo.tokyo/acl2-theorems.git/tree/)
リポジトリに置いているのでよかったら見てみてください。



### GNU Guile によるプログラミング

好きなプログラミング言語は GNU の公式の拡張言語である [GNU
Guile](https://www.gnu.org/software/guile/) です。Guile は Scheme の処理系の一つです。
日常的なちょっとしたスクリプトを書くのによく使っています。

Guile は Scheme の処理系の一つですが Scheme の処理系の中で GNU Guile を選択している最大の理由は LGPLv3
か GPLv3
でライブラリを書く文化が成立しているというところです。実際のところプログラムのライセンスを決めるときは、そのプログラミング言語のコミュニティがどういうライセンスを好むのかというので決めることも多いと思います。Guile
だとライブラリのライセンスが LGPLv3 か GPLv3 のいずれかの場合が多いし、使いたいライブラリが GPLv3 の場合は必然的に
GPLv3 を選択することになります。 よって、他のプログラミング言語と違って社会的な GPLv3 以外を使う圧をなんとなく感じることなく
GPLv3 を選択してプログラムを書くことができます。

技術的な面で GNU Guile
の一番良いところは、[末尾再帰でない手続きがスタックオーバーフローしない(システムのメモリを使い尽さない限り)](https://www.gnu.org/software/guile/manual/html_node/Stack-Overflow.html)ことです([Racket
も同じです](https://docs.racket-lang.org/guide/Lists__Iteration__and_Recursion.html))。これは明らかによいことでプログラムの書き方を変えます。一般に再帰手続きを末尾再帰に変換するのは効率のためではなくてスタックオーバーフローを恐れるためです。ほとんどの場合、末尾再帰の手続きは理解しにくく汚ないです。それに対して自然な再帰手続きは読みやすく再帰的な処理を綺麗に表現していて本当に美しいものです。よほど効率が悪くなって明らかに問題が生じてしまう場合を除けば再帰の手続きをわざわざ末尾再帰に書き換える必要はありません。末尾再帰の手続きを書くのは実質的に手続き型プログラミングをしているのとほとんど違いがないため、**普通の再帰で問題のないようなプログラミング言語こそ真の意味で関数型プログラミング言語といえるのです**。



### GPG の鍵

下記のコマンドで私の公開鍵を gpg に import できます。

    gpg --keyserver=hkps://keyserver.ubuntu.com --recv-keys C76AC7C77FF46F6E42C2D93545AA42647237561E

インポートしたら必ずフィンガープリントが下記と一致することを確認してください。

`C76A C7C7 7FF4 6F6E 42C2 D935 45AA 4264 7237 561E`



### 連絡先

[Contact](https://www.tojo.tokyo/contact.html) ページを参照してください。



### その他

  - 好きなOS・パッケージマネージャ: [GNU Guix](https://guix.gnu.org/)
      - 他のパッケージマネージャはなんか怖くて使えなくなった
          - Nix はよさそうだけど興味がなくて使えない…
      - システムのアップグレードした後に気軽に rollback できるの最高
      - guix environment を使えば簡単に開発環境の環境構築ができるのでみんなこれを使って欲しい
      - システムの設定とかパッケージの定義を GNU Guile で書けるの最高過ぎる
      - 自分用の Guix チャンネルも作って使ってる
          - <https://git.tojo.tokyo/tojo-tokyo-guix-channel.git/>
      - このサイトを表示している Web サーバーも Guix System で動いている
          - 設定:
            <https://git.tojo.tokyo/guix-config.git/tree/web/config.scm>
  - 好きなエディタ: [GNU Emacs](https://guix.gnu.org/)
      - Emacs への情熱はそこまでではないけど使っているのにはそれなりの理由がある
      - Lisp のコードを良い感じにインデントしてくれるエディタは Emacs くらいしかない
          - 他のエディタを使おうとすると Lisp のインデントができないことがすぐに致命的になる
          - [Paredit](https://www.emacswiki.org/emacs/ParEdit) が特に最高
      - [Magit](https://magit.vc/) という git クライアントがある
          - git のコマンドはあんまり覚えてなくてだいたい Magit で操作している
      - org-mode は最近使ってない……
          - Nextcloud とか Jupyter Notebook を主に使ってる
          - 何度か使う習慣を付けようとしたけど何故か私にはあんまり合っていないらしく使うのをやめてしまう
      - [Geiser](https://www.nongnu.org/geiser/) という Scheme の開発環境がある
          - GNU Guile のプログラムを書くときに使ってる
          - これがないと補完とかできないから必要
      - ACL2 でも当然のように [Emacs
        を勧めてくる](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____EMACS)
          - ただ ACL2 の Emacs の設定について理解するのには暫くかかったので Emacs に慣れている人でも最初から
            Emacs を勧めるべきかは微妙
          - 初めて ACL2 を使う場合は [ProofPad](http://new.proofpad.org/) の方がおすすめ
      - Emacs のパッケージは GNU Guix で管理するのがおすすめ
          - 複数のパッケージマネージャを管理するの大変だし全部 Guix でよい
  - 好きなクラウドサービス: [Nextcloud](https://nextcloud.com/)
      - 自分でホスティングしている
      - もはやこれなしにどうやって生きていけばいいのか分からない
      - 単にファイルをクラウドに上げるだけでなくて色々なことができる
          - [Notes](https://apps.nextcloud.com/apps/notes)
              - ちょっとしたメモを書くのに使ってる
          - [カレンダー](https://apps.nextcloud.com/apps/calendar)・[タスク管理](https://apps.nextcloud.com/apps/tasks)
              - CalDAV に対応しているので、対応ソフトウェアから利用可能
          - [News](https://apps.nextcloud.com/apps/news)
              - RSS のフィードを登録できる
          - [Maps](https://apps.nextcloud.com/apps/passwords)
              - 地図上に自分で撮影した写真を表示できるのがよい
          - [Passwords](https://apps.nextcloud.com/apps/passwords)
              - 自分で管理していないサーバーにパスワードを預けるのちょっと怖いので自分でホスティングする価値がある
          - [Bookmarks](https://apps.nextcloud.com/apps/bookmarks)
              - 複数の端末でブックマークを同期できる
  - 好きな Window Manager: [xfce4](https://www.xfce.org/)
      - タイル型ウィンドウマネージャーとかも試したけど結局私には Xfce4 が一番合っていた
      - パネルがいい
          - 私にとって必要な機能が過不足なくある
  - 使っているVPS: [Vultr](https://www.vultr.com/ja/)
      - 2017 年の 7 月からずっと使ってる
          - 他のに乗り換える理由が今のところない
      - このサイトを表示している Web サーバーも Vultr で動かしてる