# 誡之二

host 曰：即有大樂者，與悲治之。

# 深淵

Lambda 醬想遲些再去打掃房間～

# Function Calling Syntax

We use programming languages to indicate a process of actions/computations. Therefore programming languages tends to be more procedual. In other words, they are used to indicate how a thing is done.

Just as the role of verbs in a nature language sentence, an action is the most essential part of ‘doing a task’ in programming language. Of course the syntax of a programming language could be complex. I’d be here to discuss only the simplest cases of function calling among different programming languages.

# Linux 下 GFW 的 DNS 投毒解決方案

## 方案

DNSCrypt 是 OpenDNS 推出的一個用來加密 DNS 請求的代理，我用這個來繞開 GFW 的檢查。dnsmasq 是一款的 DNS 服務器，我主要用其提供 DNS 緩存的功能。

# A Brief Journal About Learning Coq

This article is completely an informal journal about my learning process on Coq. It is just created as my whim prompted. Please don’t academically refer any part of it as studying material to learn Coq.

## Pre

I first heard of Coq in my admiring mathematician, @txyyss’s tweets. At the time I saw him talked that he’s glad and immersed in re-proving all the theorems he had learned. He also said, as deepening in Coq, he found a boost on other related academic aspects. Driven by curiosity, I went to know about what a heck Coq is. Then I saw it describe itself as a ‘Proof Assistant’. I felt something uneven about it. Looking through all the programming languages I had learned, even those as logically abstract as Prolog, were not capable to do a proof.