香水の一番良いところはその香りであるよりも、その残り香であり、離れた後でもその人のことを思い出せることにある。

diary

perfume

香水を上手に使う人はすごいと思う。 どうやっても、その人のことを思い出してしまうからである。

意識的にドライにプロファイリングする時でも、その香りで判断が邪魔されてしまう。

enginnering culture

エンジニア文化はすごくドライというか、毎日勉強や訓練をすることや、リリースすることに追われてしまう側面があり、逆に人間的側面が軽視されがち。

それをエンジニア文化に属していない人からすればそれはすごく怖いところと思われがちである。

しかしながら、人間的側面が必ずあるから、私はそこを補うために活動をしているということもまた、エンジニア文化の性質を知っている人からすると、なぜ敢えてドライな文化においてそういう人間的側面を敢えて重視し、評価されないかもしれないところのことをやろうとするのか疑問視される。

人間的側面が必ずあり、そして、その人間的側面を補うことが、隣人に求められているからである。

summer school

今年の夏は京都に行けなかった。悔やまれている。

また、来年の夏もどうも行けなさそうである。それもまた後悔を産みそうであり、嫌だ。

今日の勉強

rust

TRPL

• pp. 73-80
• 所有権ではなく、引数としてオブジェクトへの参照を取る、つまり借用する関数がある
  • 実引数には&s1
  • 仮引数には&String
    • & が参照を指す
      • 参照外し演算子は*
• 変数の値を参照する参照
  • 変数の値を所有しない
  • ゆえにその参照がスコープを抜けても、その値はドロップされない
• 借用した値の変更を試みるとコンパイルエラーが発生する
  • 借用もデフォルトは不変
• 可変な参照
  • 実引数には&mut s1
  • 仮引数には&mut String
• 可変な参照の制約
  • 特定のスコープの特定のデータに対しては、1つの可変な参照しか持てない。
  • データ競合が起きる条件は以下の3つであり、これらの条件が満たされる場合に、コンパイルさえしないならば、データ競合が発生しない。
    • 2つ以上のポインタが同じデータに同時にアクセス
    • 少なくとも1つのポインタが書き込みを行っている
    • データへのアクセスを同期する機構が使用されていない。
  • 新しいスコープを生成し、同時並行でなくせば、複数の可変な参照を作れる
• 可変と不変の組み合わせでも類似の規則があり
  • 同じスコープ内で不変で借用した後に、可変で借用というのはできない
    • 不変参照の使用者は値が変わることを想定していないから
• 宙に浮いた参照
  • ダングリングポインタ
    • 他人に渡されてしまった可能性のあるメモリを指すポインタのこと
      • これはその箇所へのポインタを保持している間にメモリを解放してしまうことで発生する
  • Rustは参照がダングリング参照にならないように保証する
    • コンパイラは、参照がスコープを抜けるまでデータがスコープを抜けることがないよう確認する
      • もしそれをやろうとすると、ライフタイムパラメーターを使え、と怒られが発生する
• 参照の規則のまとめ
  • 任意のタイミングで
    • 以下のいずれか一方を行える
      • 1つの可変参照か
      • 不変な参照をいくつでも
  • 参照は、常に、有効でなければならない

team

『Team Geek』の0章、1章、そして2章の途中まで読み直す。 メモを作りつつ、近いうちの会社での発表に向けて、準備する。

• プロジェクトの成功には以下の2つの要因が必要である
  • 優れたコードという技術的要因と
  • みんなの協力という人的要因
    • 人間は難しく「人間は断続的なバグの大きな塊」
    • その一方で、チームは個人の生産性や幸福に直接影響する
• 天才の神話
  • 天才はコードを隠さない
    • 優れたコードだとしても不十分
  • コードを隠すのは不安の裏返しである
  • 天才の本当の功績は、チームとうまくやることができたこと
  • 1人でやることは失敗のリスクが高まる。みんなでやることのメリットが高い。
    • 失敗に早期に気づける
      • プロジェクトには、高速でのフィードバックループが必要
    • プロジェクトののバス係数が高まる
    • スケールできる
  • チームが全て
• 謙虚、尊敬、信頼、これを自分が持ち、相手も抱けるような環境を作ることの重要性。
  • HRT、これらが健全な対話とコラボレーションの基盤
    • これらが欠如すると人間関係が衝突する
      • 人間関係は、プロダクトやプロジェクトより、長く続く
    • これらがあると、いざ困ったときに、助けられる
  • 謙虚
    • エゴをなくす
      • コミュニティは信じられないほど強力なアイデンティティがある
    • 自分の学習のための時間を作る
  • コードの指摘には謙虚になり、相手に尊敬を含め、相手が恩恵をもたらしてくれると信頼する。
  • 失敗、学習、反復
    • 不完全を見せても構わないという謙虚さを持ち、
    • ユーザーが、対応を賞賛し、改善を要望するという信頼で、
    • 失敗の文書化(ポストモーテム)をする
      • 何を学んだか、何を改善するか
  • 忍耐を学ぶ
  • 影響を受けやすくする
    • 間違いや能力不足を認める
      • 謙虚さを見せる
    • 他人の意見を信頼する
    • この正直さと強さは尊敬を産む
• チーム文化を作ることで、自己選択的な文化になり、また、外部から来た悪意ある人や文化を排除することができるようになる。
  • 文化はイースト菌のようなもの
    • そしてその種菌が重要
  • チーム文化とは、エンジニアリングチームが共有する、経験、価値、目標
  • まず優秀なエンジニアを雇う
  • 強い文化は自己選択的な文化である
    • 文化に合わない人は、事前に遠ざかってくれる
  • 合意ベースのマネジメントなら、チーム全体が意思決定プロセスに参加できる
    • チーム全員がプロダクトの成功に強い責任を持ち
    • リーダーがチームの意見に耳を傾けること(尊敬)
  • チームメンバーの接し方
    • HRTを持っていればよい
    • 前向きな批判をしてくれる友達や同僚を見つけよう
  • 文化が、積極的なのか、のんびりなのかを理解し、
    • 新来者に支配されないように気をつけよう
• コミュニケーションなしには正しいコードを書いている保証ができない。
  • 同期コミュニケーションの人数を減らし
  • 非同期コミュニケーションの人数を増やす

Isabelle

Concrete Semantics

• Big Step Semantics with Error Propagationの定義を読む
  • 久しぶりの Concrete Semantics なので、定義の趣旨を完全に忘れている。
• Big StepにおけるDの健全性の証明を読む
  • Small Stepの場合に比べて、かなり単純になっている。
  • WhileTrueの場合の証明の部分で、command cに対する帰納法の適用を行っていることに気づくのが遅かった