Numbers in Computer Scientist's Eye
The fundation of modern mathmatics is the set theory. If you have gone through some mathmatics course, you would find that every definition comes from set directly or indirectly. For example, one poss
Home
Understanding Fix_eq in Coq
The problemWhen we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is 1
Understanding Number Representation System
There is two well-known number representation in computer: one’s complement and two’s complement. While the latter one is widely adopted almost everywhere in the computer, the former one is still used
Reasoning about programs
Summary of last yearIt has been quite a long time since my last post (which is also unfinished). Lots of things has happened and changed since last blog. I’ve been interning at Apple through the end o
Web front-end Learning notes
Realizing that I’m too weak in the front-end and lack practice. I’m determined to start to write a SPA this winter holiday. This post is intended to note down some discoveries during development. Meta
Fedora configuration
This is only notes for myself. Not the best practice and not for anyone else. PreconfigurationInstall fedy as soon as possible, which save you of a lot of troubles. 1bash -c 'su -c "curl http://folksw
Vagrant and Virtualbox
Notes only, not best practice Mount protocol error1sudo ln -s /opt/VBoxGuestAdditions-*/lib/VBoxGuestAdditions /usr/lib/VBoxGuestAdditions Mount: No such devicestart the virtual machine in the virtua
iptables and firewalld tricks
CauseSome libev port version of something does not support the --forbidden-ip option. To avoid SMTP abuse, originally I moved back to the python version of it. Later I found python version has some bu
Python3.5+Tornado
期末考完一塌糊涂于是开始埋头写代码 正好pm iceboy开始了vj4项目，就顺便学习一下python好了 Day 0今天装好了系统，不过感觉centos真不友好，各种版本低全部要自己编译安装，还是fedora大法好。 装了一个velocity看起来挺好用的，本来以为只有查看api的功能，结果发现tornado的整个readthedoc都被缓存下来，可以直接看教程。 热烈盼望换上mbp就能有das
LaTeX and more
Since LaTeX is recommanded in VV186 and many other courses and LaTeX is unfriendly to newbies, I’m going to share my LaTeX writing style. ShareLaTeXShareLaTeX is an online LaTeX editor, and even mor