先來點實際的

看了那麼久的 pi-calculus 還是覺得離 concurrent programs 很遠（例如一個 MVar 應該是個 process 而不是單純的 channel 吧？），如果就卯起來寫 Agda modelling of pi-calculus 好像沒什麼意義。所以我還是先在紙上練習 programming in pi-calculus，湊一點實際的東西出來吧。而且我有點懷疑 pi-calculus 對於實務目的太過 primitive，就像沒有人會用 lambda-calculus 寫 practical programs 一樣。所以現在正在讀 Pict 的 tutorial，看看它怎麼把 pi-calculus 變成 practical PL。（它是吧？XD）

--
幸好隨機客還認我當專題生 XD。

---

果然有嚴重問題。首先我不知道要該寫什麼 concurrent program。Dining philosophers、bakery algorithm 那一類的好像都不太對勁。再來別說程式，就連 specification 會長什麼樣子都不知道…

--
Pict 又挺詭異的…