PCを買うよりも新しい机を買おうと思い直した。

PCを新調しようと定期的に思いついてしまうが、いや、結局今のマシンでも十分であるし、その金で机を新しくしたほうがいいと思い直した。 (つよつよPCを作るくらいなら、AWSでremote 開発環境を作った方が安く済む。また、PCの資産としての価値は低いから。)

現在の机はIKEAのもので、だいぶぼろぼろになっている。また、机の広さも足りなさを感じている。

diary

午前中。

チキンのトマト煮を作った。 間違えてカットトマトではなくホールトマト缶を買っていたことに気づいたが、うまく作れた。

FEBCで日曜礼拝を聞く。

午後は頭痛がひどくて、そして虚無が襲い掛かってきた。何にも手がつかなくなった。

感情をコントロールするためには、体を動かす必要があるが、その気持ちすらわかない場合にどうすればいいのだろうか。

愛の実現のために

信仰は望んでいる事柄を確信し、見えない事実を確認すること。つまり、神の存在や神の愛を確認できる。

行いが伴わないなら、信仰はそれだけでは死んだもの。信仰という心から神へ愛を伝えるチャネルを成長させるためには、行い・活動が必要である。信仰が愛を導き、行動がその愛の実現を導く。 御言葉を読み、神が私達の魂に入り込む様を見、祈るという行動こそが、神様に愛を本物で成熟したものへと涵養する。

私達が神を愛するのは、神がまず私達を愛してくださったから。神からの愛は、信仰や行動による報酬ではない。

私は他人とその心や魂の存在を疑っている。だから、他人を愛することへの確信がない。だから、信仰を持ち、行動をし、神を通して、その存在に確信を持ち、愛を実現させる。

今日の勉強

sml

『Standard ML 入門』

isabelle

Concrete Semantics

カンニングしてわかったこととして、以下の書き方がある。

proof (csses)
    assume "A"
    ...
next
    assume "\not A"
    ...
qed

と同じことは

proof (csses "A")
    case True
    ...
next
    case False
    ...
qed

というのが使えることがわかった。