今日は休息の日とした

diary

rest

休むことは良いことと自分に言い聞かせる。

hat

帽子が欲しい。Jewish Hatが欲しい。

昨日、西武に行ったら対して良さげでもないものが、3万超えていた。やはりユダヤ教徒が普段使う落ち着いた帽子が丁度良いと思う。

今日の勉強

team

リーダーシップパターン

エゴをなくす
- 謙虚になること
  - 犠牲になることではない
  - 地震があにことでもない
- チーム全体のエゴやアイデンティティを育もう
- 方法:
  - チームを信頼すること
    - リーダーの仕事:
      - チームの合意形成や方向性の決定を支援
        質問を歓迎し、オープンに受け止める
    - リーダーの仕事ではないこと:
      - 全てに正しく
      - 全てを知り
      - 全てに応える
      - 達成方法はプロダクトを作る人が決定すべき
  - ミスをしたときに謝ること
    - 心から謝罪するということ
      - 分別があり、状況判断が得意で、ＨＲＴのＨを備えた人と思われるようになる
禅マスターになる
- 多くのエンジニアが懐疑的や批判的な感度が高いと思われる
  - チームリーダーとしてはそういった言葉を慎め
- 常に平静を保つ
  - そうでないと部下に大きな悪影響を及ばす
- 問題解決モードに突入する前に、質問者の問題解決を助けるために支援をする
  - そのために質問をうる
触媒になる
- 合意の形成を行う。
  - 方向性を示したり、決定したりする
- 妨害や障害の除去・回避
  - 適任者へ連絡する
  - 適切な答えを知るよりも、適切な人を汁方が価値がある
- 安心感を与え、リスクを取れるようにする
  - リスクをとれば大きな成功の確率が上がったり、道が開けたりする
  - 失敗してもいいことをチームに知らせる
    - 失敗によって多くのことを素早く学べる
  - 個人の成功はみんなの前で称え、
    - 失敗はチームとして受け止め、そこから学ぶ
    - プライベートで建設的な批判をする
先生やメンターになる
- 自力で学ばせようとするのがリーダーの大切な役目
  - 学ばせること:
    - 技術
    - コード
    - チーム文化、
    - 想定される責任レベル
- メンターに必要な三つのこと
  - チームのプロセスとシステムの経験
  - 誰かに教える能力
  - 相手がどれだけ支援を必要としているかを把握する能力
目標を明確にする
- チームメンバーが同じ方向に行かねばならない
- ミッションステートメントを見せる
  - あとは、自律性に任せて、定期に敵に確認
  - これで、チームの効率は劇的に向上する
正直になる
- 褒め言葉のサンドイッチを避けた方がいい
- 本当に伝えたいメッセージを、正しく伝わっていることが重要
  - 建設的な批判をするときは、親身になって共感すればいい
  - 失礼のないように明確に
  - 相手を防御的にするような伝え方はしない
幸せを追い求める
- リーダーとして長期にわたって生産的に、かつ、離脱者を少なくするには、時間を作って、チームの幸せを計測すればいい
- 一対一の面談の後に「何か必要なものはある？」と質問する
- オフィスの外におけるチームの幸せにも注意を向けた方がいい
  - どうして生産性が高いのか低いのかが、プライベートな状況にまで目を向けているか、わかるかも
- 暗黙的な目標を明確化する
他のリマーク
- 移譲せよ、ただし手を汚せ
  - 誰もやらないような仕事を担当してみる
- 自分自身を置き換えようとする
- 事を荒立てる時を汁
- カオスからチームを守る
  - チームの外側のカオスと不確実性と狂気がある
- 新しいことをやりたいなら取返しがつくかどうかを見極める
- チームを空中援護する
- いいところをフィードバックする

isabelle

証明すること:

fold c empty ~ c

求められること：

empty tableから任意のtableに一般化する
tに対するside conditionの追加
conditionを除いてコマンドが等しい
- commandの等しさは、
  - 全てのstateではなく、
  - preconditionを満たすstateについて、
  - 実行が一致することが求められる

equiv_up_to:

p |= c ~ c'
    = 
ALL s s'. P s --> (c,s) => s' = (c', s) => s'

bequiv_up_to:

p |= b <~> b'
    = 
ALL s . P s --> bval b s = bval b' s