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