# 研究目的

• アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
  • しかしOSの機能をテストですべて検証するのは不可能である。
• 定理証明やモデル検査を利用して、テストに頼らずに保証したい
  • 証明しやすい形、かつ実際に動くソースコードが必要
  • 継続ベースの状態遷移系で再実装することで表現しやすくしたい
• プログラムは二つの計算に分離される
  • プログラムは入力と出力の関係を決める計算(ノーマルレベル)
  • その計算に必要なメタな計算(メタレベル)
• プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
• そのためにはメタレベルの計算を柔軟に扱うAPIや実装方法が必要
• 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。

# 今週

• シス管周りいろいろ
  • news-ieにCMSを仕込んだ
  • あとで通知を作成
• 余裕が出てきたのでいろいろ再開
  • ie-virshを構築したいけど、C + Python2なのでどうせならRustで書き直すかみたいな気分
  • Rust忘れてたのでRustlingsやってた
  • https://github.com/rust-lang/rustlings

# Gears系

• par gotoの高速化ちょっとやろうかなみたいな気持ち
  • その前にcontextへの書き戻しを検知 or 構文で書き戻しを禁止したい気がする