めたせぴ2015☆ゆく年くる年 草稿
-
masterq_mogumog
- 1130
- 1
- 0
- 1
-
- いいね！1
I moved to Mastodon.
@masterq_mogumog
関数型IoTプログラミング勉強会 fpiot.doorkeeper.jp/events/34203 を来年は継続的に開くこと。できれば毎月ペースで。この中では関数型言語にとどまらず、他の形式手法についても広く扱うことにしたい。「ネタに漬きず息切れしない」ことを目標にしたい。
2015-12-30 21:26:12
I moved to Mastodon.
@masterq_mogumog
なんでこんなことをするのか、というと組み込み開発に使える言語や形式手法について俯瞰できる文献が圧倒的に不足しているという危機感があるから。僕等末端の設計者としては安全な設計が得られれば手法はなんでもいい。JSで安全な設計が得やすいのなら、それもまたありかもしれない。
2015-12-30 21:27:45
I moved to Mastodon.
@masterq_mogumog
そいういう意味ではモチベーションを説明することに初回は使った方がいいのかもしれない #関数型IoTプログラミング勉強会 #苦手
2015-12-30 21:28:22
I moved to Mastodon.
@masterq_mogumog
この勉強会ではarduino-atsみたいなプロジェクトをポコポコおこして、縦軸:ソフトスタック/横軸ハードプラットフォームのような表にわけて管理したい。
2015-12-30 21:30:09
I moved to Mastodon.
@masterq_mogumog
例えばATSやIvoryは8-bit/16-bit/32-bitで使えるけどjhcは32-bitでしか使えない、というような、そんなおおざっぱなまとめをしたい
2015-12-30 21:30:49
I moved to Mastodon.
@masterq_mogumog
#今僕に見えないもの という点では #seL4 と #VeriFast だと思う。後者は楽にサーベイできそう。前者はけわしい。他にも見えないものを洗い出すのに”Related Languages”を参照した方がいい / whiley.org
2015-12-30 21:34:15
I moved to Mastodon.
@masterq_mogumog
ああ。あとICFPのついでにHongwei研に行ってきたんだった。正直ICFPで病んでたので、こっちの方が収穫が多かった / #ATS2 の作者Hongwei Xiの研究室に行ってきたよ - Togetterまとめ togetter.com/li/867083
2015-12-30 21:35:54
I moved to Mastodon.
@masterq_mogumog
なんとなくHongwei研でやってることが組み込みよりからJS実行を前提にした型の使い方(セッション型など)にシフトしつつあるのが、少し心配。ネタがそっち方面なのはわかるんだけど、、、
2015-12-30 21:37:24
I moved to Mastodon.
@masterq_mogumog
あとは関数型言語プログラマが小規模マイコンで開発できる下地となるナレッジをこの勉強会でいろいろ作っておきたい。ボード買ってきて、Lチカするところまでは一日あれば終えられるように / 関数型IoTプログラミング勉強会 fpiot.doorkeeper.jp/events/34203
2015-12-30 21:39:00
I moved to Mastodon.
@masterq_mogumog
そういう意味ではメジャーなプラットフォームをサポートしてあげることなんだけど、、、#Arduino #mbed #ESP8266 ぐらいかなぁ。。。
2015-12-30 21:39:50
I moved to Mastodon.
@masterq_mogumog
#ESP8266 のファーム書き換えが日本でちゃんと認められればあるいは選択肢をせばめられるという。。。
2015-12-30 21:40:22
I moved to Mastodon.
@masterq_mogumog
あとは論文どうすっか、ってのはある。仕事で無理矢理ATSを使ってしまって、CUFP cufp.org という手があるのですが、自分の幸福のために他人を不幸にはできないのでした。。。
2015-12-30 21:41:53
I moved to Mastodon.
@masterq_mogumog
#VeriFast での商用事例を作ったら、どっかの国際学会に捩じ込めないものなんでしょうか。。。そもそもどーゆー学会があるのかわからないので、アレです。。。
2015-12-30 21:42:28
I moved to Mastodon.
@masterq_mogumog
そういう意味ではPPLあたりに出してみて、詳しい人の助言をもらうのがまわり道だけど確実なのかもしれないですね。。。
2015-12-30 21:43:03
I moved to Mastodon.
@masterq_mogumog
あと、当初の予定だと何があったかなぁ。。。 / metasepi.org/map.html#mind-…
2015-12-30 21:45:24
I moved to Mastodon.
@masterq_mogumog
あーMico8 latticesemi.com/Products/Desig… を使った型によるハード/ソフト協調設計というのはやってみたかったけれど、いやぁ、もう、完全にまた来世。。。
2015-12-30 21:47:02
I moved to Mastodon.
@masterq_mogumog
ATSのDWARF対応をしてgdbでデバッグしたいというのもあった。。。優先度が低くなってしまい未達。。。
2015-12-30 21:47:40
I moved to Mastodon.
@masterq_mogumog
ATSのような言語をZ3を使って作る、というネタもあるのでした。これは #VeriFast をサーベイすればかなりの部分見えるようになると思う
2015-12-30 21:48:15
I moved to Mastodon.
@masterq_mogumog
Unixライクkernelの設計にqueue theoryを導入するというのもやってみたいけど、証明駆動開発が上手くいってからだなぁ。
2015-12-30 21:49:16
I moved to Mastodon.
@masterq_mogumog
スナッチ開発をするベースとしてはLinuxを選んでいたけど、関数単位でのスナッチが上手くいかないケースが多いことに気がついて、見通しの良いNetBSDに再度かたむきつつある。NetBSDのどの部分を粒度の荒い書き換えをすべきかは良く考えた方がいい。TCP/IPとかその単位で
2015-12-30 21:51:08
I moved to Mastodon.
@masterq_mogumog
小規模RTOSベースにして証明駆動開発の効果を見るならchopstx git.gniibe.org/gitweb/?p=chop… が良いと思う。小さい。これなら全体を一気に再設計するのも簡単。悪いけどTOPPERSはお金がないとやらないぉ。
2015-12-30 21:53:48
I moved to Mastodon.
@masterq_mogumog
MINIXはどうなんでしょうか。。。最近の動向を知らないので、実用化度合いがどんなんなのかわからないのです。。。
2015-12-30 21:54:40