-
masterq_mogumog
- 2463
- 1
- 1
- 12

「Xanaduは悪いアイデアだったのか?」「DML=>Xanadu=>ATSのようにコンパイラは成長した。Xanaduで採用したC言語文法は型表現に対して柔軟ではなかった」C言語文法の方がユーザフレンドリだけどしょうがないのかな cs.bu.edu/~hwxi/Xanadu/X…
2015-08-30 00:49:38
「読むべきソースコードのリストはあるか」「今はセッション型のコードがおすすめ。現状はErlangバックエンドに対する実装がある。C言語でも相当のC言語コードサポートを書けば使えるはず」 github.com/githwxi/ATS-Po…
2015-08-30 00:52:04
「セッション型の実装ではボイラープレート対策のために #codegen2 という新しいキーワードを使っている。これはHaskellのderiveのようなことができるが、テンプレートを使っているためその挙動を細かくユーザが調整できる」 github.com/githwxi/ATS-Po…
2015-08-30 00:54:34
「コーディングスタイルはどうしてあんななの?型シグニチャの宣言はあれでいいけど、インデントはつけてよ。日本のユーザにはフォーマッタ作る動きさえあるよ」「フォーマッタ作るのはいいね!」はぐらかされた。
2015-08-30 00:56:04
「将来的にC言語側でのエラーをATS側のエラーに持ち上げることは可能なのか。今のC言語側でのエラーはわかりずらい」「C言語側でのエラーをATS1のようにもっとわかりやすくすることは可能だと思う」
2015-08-30 00:57:30
「丁度良い証明コード量とは?多すぎると証明が大変。少ないとコードが危険」「Z3を使った自動証明が可能になるケースはあると思う。ただし、証明できなかったときに型エラーから判別するのは困難になるだろう」つまり半自動の証明作ってもパラダイスがひろがってる訳じゃないってことですね。。。
2015-08-30 00:59:15
「ATS1時代の思い出ある? ATSfloat scg.ece.ucsb.edu/ats.html とかあったけどあのユーザ層はどこいっちゃったの?」「ATSfloatは僕とは別に開発していた。最近はコンタクトがないね」やっぱりATS1=>ATS2の移行でかなりのユーザが消えたのでは
2015-08-30 01:01:30
William Blairから。「Habitっていう組込Haskell実装があるよ hasp.cs.pdx.edu 」「ぼくの古いAVRなどの記事は blogs.bu.edu/wdblair/ から読めるよ」
2015-08-30 01:04:53
「セッション型は多数のホスト間でのプロトコルやメニーコア上のコードなどに有効。最近はAmazonがお金を出して研究している。君も parallella.org とかで #ATS2 のセッション型を使ったアプリケーション作ってみるのもいいんじゃない?」
2015-08-30 01:06:20
「ボストン大学でドイツの組み込みOS規格にのっとったOSを作っていて、その上で動くアプリケーションを #ATS2 で書くこころみをやってみたことがある。この時はOS実装そのものはC言語で書いた」
2015-08-30 01:09:54
「証明コードを書くときは、あまり束縛名を上書きしない方が良い。型エラーがどの束縛に対するものなのかわかりにくくなる。」
2015-08-30 01:11:05
ミーハーだけど写真取った。左から Steinway Wu, Hongwei Xi, 僕, William Blair pic.twitter.com/TpWA3jaGgW
2015-08-30 01:14:37

Hongweiの研究室に行くには、この地図にしたがって歩いて、、、 pic.twitter.com/URY8KmJvHz
2015-08-30 01:15:53

二回の287をノックしよう pic.twitter.com/12vI4Wd3gA
2015-08-30 01:16:45

ボストン大学でATS言語アプリケーションを作った際のドイツの組み込みOS規格のRTOSはOSEKだった。思い出した。 / OSEK - Wikipedia, the free encyclopedia en.wikipedia.org/wiki/OSEK
2015-09-28 21:47:07