# 2020/11/10

# 研究目的
- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
    - しかしOSの機能をテストですべて検証するのは不可能である。
- 定理証明やモデル検査を利用して、テストに頼らずに保証したい    
    - 証明しやすい形、かつ実際に動くソースコードが必要
    - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
- プログラムは二つの計算に分離される
    - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
    - その計算に必要なメタな計算(メタレベル)
- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
- そのためにはメタレベルの計算を柔軟に扱うAPIや実装方法が必要
- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。
    
    
# 今週
- 奨学金の免除申請の書類が来たので作文をすることに
    - 業績系いろいろ書かないと...
    - 指導教員の推薦の作文がありますがどうしましょう...
- 知り合いのエンジニアが沖縄に来てたので飲みに行っていた    
- アシャリフ先生のpukiwiki置換
    - ひたすらperlを書いてeuc-jpにキレる世界観    
- RustのFileWriteを書いた    
    - https://gitlab.ie.u-ryukyu.ac.jp/os/2020/k198584/filewrite    
- Rakuのenv系のビルドツールにプルリクを送ったけれど無視されて辛い    
    
# CbC関連

- B3の松岡くんと作業した
- ArmなCbC GCCのdependendsで指定していた`arm-none-eabi-gcc`が古いらしい

```diff
diff --git a/cbcgcc-arm.rb b/cbcgcc-arm.rb
index 5bd5e81..8823374 100644
--- a/cbcgcc-arm.rb
+++ b/cbcgcc-arm.rb
@@ -14,7 +14,7 @@ class CbcgccArm < Formula
   depends_on "mpfr"
   depends_on "libmpc"
   depends_on "zstd"
-  depends_on "arm-none-eabi-gcc"
+  depends_on "ArmMbed/homebrew-formulae/arm-none-eabi-gcc"
 
   bottle do
     rebuild 1
@@ -43,7 +43,8 @@ class CbcgccArm < Formula
          "--disable-werror",
          "--disable-libssp", "--disable-libstdcxx-pch", "--disable-libmudflap",
          "--with-newlib",
-         "--with-headers=#{arm}/gcc/arm-none-eabi/include,#{inc}"
+         "--with-headers=#{arm}/gcc/arm-none-eabi/include,#{inc}",
+         "--with-gas"
       system "sh config.status"
       system "make","-j","4"
       system "make", "install"
```

# Raku関係

Rakudo-Star(rakuの季節ごとにでる詰め合わせパック)のビルドツールが`Configure.pl`から`rstar`に変更になっていた。

- MoarVM, NQP, Rakuのそれぞれでは`Configure.pl`が使われているらしい
- `rstar`はbash script

気づいたら`v2020.10`に...

- https://twitter.com/koto_san_kana/status/1320121190724341760

```shell
$raku --version
Welcome to 𝐑𝐚𝐤𝐮𝐝𝐨™ v2020.10.
Implementing the 𝐑𝐚𝐤𝐮™ programming language v6.d.
Built on MoarVM version 2020.10.
```