Telegram Group & Telegram Channel
#书

每年的4.23是世界读书日,推荐一本过去一年在精读的技术书《Types and Programming Languages》(简称TAPL)。

我与这本书的缘分是这样的:

最开始,想要看懂databend里面的表达式系统代码,看迟先生的类型体操系列文章《用 Rust 做类型体操》,发现看不懂。

于是请教了负责表达式系统的同事,给我推荐了TAPL这本书。

开始阅读TAPL,但是发现里面很多符号看不懂,需要补一些数理逻辑和Lambda演算的基础。

补习了上述基础之后,继续看TAPL,能看懂部分了。第一刷TAPL花了半年多的时间(包括补习基础的时间)。

现在又重新整理了一下之前做的笔记,也看了部分EOPL(全称“Essentials of Programming Languages”)的内容,开始第二刷。在完善了前面的基础之后,第二刷就流畅很多了。

这个过程中有如下的收获:
1、体验到了数理逻辑形式化的美感。做工程的时候,经常会做工程上的trade-off,但是在类型系统这里,一个类型能否转换为另一个类型,需要严谨的推导,可以就是可以,不行就是不行,不存在trade-off。我特别喜欢这种符号形式化、确定性的美感。
2、重拾了对PL的兴趣。我接下来会把EOPL和TAPL刷完,打算接着学习一下OCaml,再看看能不能给Rust贡献一些代码。
3、后面会学习抽象代数和范畴论,学习范畴论是为了更好理解PL里面的一些理论。
4、Rust最开始吸引我的是它的内存安全特性,现在除此以外,还有它强大的类型系统,强类型系统的语言写起来放心、方便很多。我后续可能不太能接受用非强类型的语言来做为主力编程语言了。

为了纪念这个学习的过程,我前两个月趁着JD搞活动,花重金(大几百人民币)买了一本TAPL原版书,五一之后就能送到了。



tg-me.com/codedump_notes/555
Create:
Last Update:

#书

每年的4.23是世界读书日,推荐一本过去一年在精读的技术书《Types and Programming Languages》(简称TAPL)。

我与这本书的缘分是这样的:

最开始,想要看懂databend里面的表达式系统代码,看迟先生的类型体操系列文章《用 Rust 做类型体操》,发现看不懂。

于是请教了负责表达式系统的同事,给我推荐了TAPL这本书。

开始阅读TAPL,但是发现里面很多符号看不懂,需要补一些数理逻辑和Lambda演算的基础。

补习了上述基础之后,继续看TAPL,能看懂部分了。第一刷TAPL花了半年多的时间(包括补习基础的时间)。

现在又重新整理了一下之前做的笔记,也看了部分EOPL(全称“Essentials of Programming Languages”)的内容,开始第二刷。在完善了前面的基础之后,第二刷就流畅很多了。

这个过程中有如下的收获:
1、体验到了数理逻辑形式化的美感。做工程的时候,经常会做工程上的trade-off,但是在类型系统这里,一个类型能否转换为另一个类型,需要严谨的推导,可以就是可以,不行就是不行,不存在trade-off。我特别喜欢这种符号形式化、确定性的美感。
2、重拾了对PL的兴趣。我接下来会把EOPL和TAPL刷完,打算接着学习一下OCaml,再看看能不能给Rust贡献一些代码。
3、后面会学习抽象代数和范畴论,学习范畴论是为了更好理解PL里面的一些理论。
4、Rust最开始吸引我的是它的内存安全特性,现在除此以外,还有它强大的类型系统,强类型系统的语言写起来放心、方便很多。我后续可能不太能接受用非强类型的语言来做为主力编程语言了。

为了纪念这个学习的过程,我前两个月趁着JD搞活动,花重金(大几百人民币)买了一本TAPL原版书,五一之后就能送到了。

BY codedump的电报频道




Share with your friend now:
tg-me.com/codedump_notes/555

View MORE
Open in Telegram


codedump的电报频道 Telegram | DID YOU KNOW?

Date: |

If riding a bucking bronco is your idea of fun, you’re going to love what the stock market has in store. Consider this past week’s ride a preview.The week’s action didn’t look like much, if you didn’t know better. The Dow Jones Industrial Average rose 213.12 points or 0.6%, while the S&P 500 advanced 0.5%, and the Nasdaq Composite ended little changed.

Why Telegram?

Telegram has no known backdoors and, even though it is come in for criticism for using proprietary encryption methods instead of open-source ones, those have yet to be compromised. While no messaging app can guarantee a 100% impermeable defense against determined attackers, Telegram is vulnerabilities are few and either theoretical or based on spoof files fooling users into actively enabling an attack.

codedump的电报频道 from kr


Telegram codedump的电报频道
FROM USA