Shou's origin

Source of everything

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.

夢魘

晚上,我在墳地挖土,點上火炬。
頭頂的火光把周圍照得通明。

我抓著幻想中的水平懸絲,
在各式燒給他們的物件中跳躍。

到白天,這裡卻成了一座鬼城。
四處盡是餐館酒店,一片繁華。

Setting Up IP Over ICMP With Hans

Background

The ISP, China Telecom, interrupted the internet access from my home yesterday due to the expiration of annually subscription of the internet service. While I found that ICMP packets are not blocked. Even though I can’t even do a DNS query, I can ping any server as usual.

The inaccessibility of internet has greatly evoked my anxiety on seeking changes. Well, it’s theoretically possible to carry data in ICMP packets. Therefore, according to the hacker community’s principle, there should already been hackers who made use of this and opened the sources of their programs.

Indeed, searching ‘ICMP tunneling’, I found hans and icmptx. The latter one is more primitive and complicated to use. After several trials and failures, I decide to give icmptx up, and try hans instead.

This article is a tutorial/note about how to establish normal internet connection in the condition that only ICMP packets are allowed to pass through the firewall with hans.

Experience About Contributing KDE Projects

It’s the first time I am involved in contributing KDE, and I think that’s very wonderful experience for me.

The first task I claimed is convert the all class members in calligra/kexi project to d-pointers. This task is not very hard to me actually. Because that the source files and classes are so many, it takes most of labors, and some experiences and ability to to cope with exceptions. I’ve been leaving c++ for almost one year time, so totally the most important thing I gained is to pick up c++ again. Further more, I don’t used to know to use d-pointers to reduce coupling, and now I learnt it, which is really cool.

Then I’ve contributed with marble-globe task. The task is about adding remote icon/image support for marble. I got known about the typical structure of a KDE programs, and I’m feeling like to program Qt, which is really powerful and handy. And then by the passion, I wrote the required KML tag writers for marble, too. These are interesting for me.

Totally speaking the greatest gain is the achievement of contributing open source projects. This is biggest open source project I’ve been involved in, since before I used to just collaborate opensource project with small groups or individuals on github before. Those hackers I met are really friendly. I’m very careless. I made a lot of mistakes, and even didn’t realize that. At those times, my mentor always explained to me patiently & gently, that made feel embarrassed when finally I knew that’s my fault. And at the time, when I met project-related problems that I can’t solve and not able to be abstracted to ask on stackoverflow, I sent emails to my mentors and they explained the reason of the problem clearly and gave me guidance to solve it. I can feel that the hackers in open source community are glad to help those beginners like me, and that’s really impressive for me.

This is the first time & will be the last that I could attend Google Code-In, but I will continue work on contributing open source projects. I love the atmosphere in open source communities and I would like to get acquainted to more hackers. Good luck.

That’s it, thanks to all.

祭獻

我在黑暗中醒來
不能看到任何東西
我和一切無關
因此意識遠遠離開了這個世界

朝曦

我注視著妳的眼睛
我看不到光芒

我望到了我自己,在飽受折磨
那是茫茫的天空
彷彿甚麼都不存在

挑戰龍的勇士

我崇敬挑戰龍而失敗的勇士,
而不是皇帝。

我期待的是一種平衡,
一種可以維持永久的,
自然而包容萬物的平衡,
將世界置於其中,
然後,把發現者燒死。

April 2012

Another month as you see.

While it seems that I changed nothing and actually base on Mutation I was a completely new guy from the previous second.

Leave the useless words aside, I’m not a mutant as I always concern. Yes, I know you all do not think how it does matter, while you should know, I just seem like a bare body with soul losted(I’m sorry as Mutation does not support souls), and rather, I could touch the soul as it is just in the front, and watch completely throughout all that stuff but, what the most important thing is that the goddamn soul does not ever belong to it.

I walked out from the shadow, but I didn’t see the light. Just like a fish that got to the dryland, with loneliness and helplessness.

February 2012

10 months remaining.

Well, the month could be summarized as the word ‘dream’.

Since the short dreamworld control last month, I have been experienced up to five or six times of wonderful dreamworld controls. Not exactly, some of my dream, actually, are nightmare, while the protagonist knows who himself is.

And currently I’m keeping to write my cscript, which will be a script language with c-like syntax.

While the period, I learnt some yacc/lex and some tricks from that.

For programming, I even touched a bit Ruby and django framework for python.

I was cured, all right!

完美世界

這就是亞首的生平.

亞首發現自己在一個地方.

亞首擁有思想, 但無法控制這身體, 他通過眼睛觀察這個世界, 然而看到的是模糊的一片混沌, 什麼也沒有.

當亞首想方法向這個世界的表示他的想法, 這個身體卻完全不受他的控制, 他感到很不舒服. 他的大腦結構非常簡單, 甚至令他難以進行稍微高速一點或者複雜一點的運算.

他想的東西太多的時候, 會受不了, 然後在不知不覺中睡著.

他竭力向這個世界表示自己不是白癡, 卻做不到, 一切都完全受到動物本能的控制.

他不知道發生了什麼事情.