めたせぴ2015☆ゆく年くる年 草稿
-
masterq_mogumog
- 1116
- 1
- 0
- 1
-
- いいね！1
I moved to Mastodon.
@masterq_mogumog
なんで「証明的な線形マージソート」を使いたかったのか、というとmallocが使えないArduino Unoの上で証明駆動開発が機能することを立証したかったから。
2015-12-30 20:35:05
I moved to Mastodon.
@masterq_mogumog
このこころみに失敗したので、ML Workshopでの僕の発表はほんとうにショボいものになってしまった。ICFPの期間中、ずっとダークサイドに落ちていました。。。
2015-12-30 20:35:46
I moved to Mastodon.
@masterq_mogumog
10/24-11/6までの間、このリポジトリではその後ジャンケンゲームを作っていたようです。 github.com/jats-ug/practi… このコードは slideshare.net/master_q/stati… で発表しました。
2015-12-30 20:38:09
I moved to Mastodon.
@masterq_mogumog
証明付きインプレースマージソート、悔しいので、スクラッチからもう一回挑戦したい。。。
2015-12-30 20:40:58
I moved to Mastodon.
@masterq_mogumog
最初から証明付けたのが敗因だったと思う。最初は線形型だけ使って楽に設計して、後から証明を付ければあるいは。。。
2015-12-30 20:41:31
I moved to Mastodon.
@masterq_mogumog
Mikeのことを思い出そうとしているんだけど、ピンポイントのメールが出てこないぞ。。。
2015-12-30 20:50:31
I moved to Mastodon.
@masterq_mogumog
Mike Jonesという新入りがいきなりATSメーリングリストに降臨する。どうもArduino+ATSで製品開発をしているっぽい。Hongweiちゃんの手解きでATSに良い感触をもってくれたようで、たいへん嬉しかった / groups.google.com/forum/#!msg/at…
2015-12-30 20:53:00
I moved to Mastodon.
@masterq_mogumog
MikeのこのPros/Consまとめは、ATSの初学者にとってかなり参考になると思う / groups.google.com/forum/#!msg/at…
2015-12-30 20:53:50
I moved to Mastodon.
@masterq_mogumog
11/5にechronos OSに少しだけ興味がわいたみたい。echronosはまだ開発途中なのでseL4をサーベイした方が良いというのが今の感触 / Where is verification code? · Issue #13 github.com/echronos/echro…
2015-12-30 20:56:08
I moved to Mastodon.
@masterq_mogumog
12/1-12/5までの間、Ivory ivorylang.org を使ってArduinoプログラミングをしていた。IvoryにはNULLポインタを作れない型付きC言語程度の力しかないと思っている。自分の中では github.com/fpiot/arduino-…
2015-12-30 20:59:14
I moved to Mastodon.
@masterq_mogumog
「Haskell界に戻ってきたの？」と聞かれて少し答につまりました。。 / Top level Makefile is broken? · Issue #59 · GaloisInc/ivory github.com/GaloisInc/ivor…
2015-12-30 21:00:56
I moved to Mastodon.
@masterq_mogumog
12/6あたりにsmart.jsという小規模マイコン向けJavaScript環境を弄っていたみたい。GC付き言語をマイコンで使うのには少しアレだけど、cesantaのミドルウェアは優秀だと感じた。仕事にも使いたい / github.com/cesanta/smart.…
2015-12-30 21:03:34
I moved to Mastodon.
@masterq_mogumog
12/22にVeriFast people.cs.kuleuven.be/~bart.jacobs/v… という検査ツールでArduinoプログラミングをするプロジェクトを作った。まだ単純な引数/返り値検査しかしていない。この検査器には将来性を感じている / github.com/fpiot/arduino-…
2015-12-30 21:06:32
I moved to Mastodon.
@masterq_mogumog
VeriFast people.cs.kuleuven.be/~bart.jacobs/v… はC言語のコメントに事前/事後条件を埋め込むと検査をしてくれる。malloc/freeエラーも検出。どうもコメントに書ける関数はATSで言うところの証明関数のようなもののようだ。線形型との関連はまだわかっていない
2015-12-30 21:07:48
I moved to Mastodon.
@masterq_mogumog
VeriFast people.cs.kuleuven.be/~bart.jacobs/v… を使ったArduinoプログラミングにはもう一ヶ月程度費やす価値はあるように感じています。残念なのは検査器がOSSではないということですが、、、しかし言語アイデアの種にはなると思う。
2015-12-30 21:08:49
I moved to Mastodon.
@masterq_mogumog
あ、smart.jsに関連するcesanta製ミドルウェアについては slideshare.net/master_q/smart… を参照してください。
2015-12-30 21:10:24
I moved to Mastodon.
@masterq_mogumog
11/5-11/29の間 ESP-WROOM espressif.com/en/products/wr… 上で動くATSプログラムを作っていたみたい。IFTTT経由でTweetとかできるようになったので、良い感じのデモ動画は撮りたい / github.com/fpiot/esp8266-…
2015-12-30 21:13:55
I moved to Mastodon.
@masterq_mogumog
今年の前半は #証明駆動開発 のコストの高さをようやっと実感できるようになったと言えるんじゃないだろうか。その理由も具体例を使って他者に説明できるようになったんだと思う。プロジェクトは全く前に進んでいないけど、僕自身の中は変わった。
2015-12-30 21:19:15
I moved to Mastodon.
@masterq_mogumog
だから、大規模な組み込みプロジェクト全体を #証明駆動開発 できるのか否か、という点について非常に懐疑的になった。少なくともATSの証明器を使うのは効率が悪すぎると感じるようになった。
2015-12-30 21:20:16
I moved to Mastodon.
@masterq_mogumog
Coqだとどうなるか、という点はわからない。。。タクティクが使えるのはすばらしいですね。
2015-12-30 21:21:23
I moved to Mastodon.
@masterq_mogumog
大規模な組み込みプロジェクト全体に対する #証明駆動開発 はseL4 sel4.systems をサーベイすれば見込みが得られるという感触はある。だからseL4の証明コードを読むのは来年やった方がいいだろう
2015-12-30 21:22:23