Once I compiled programs.
Later I wrote proofs about programs.
Now I compile programs with proofs.
One day I hope to compile proofs and get programs.
(I want to be @pigworker when I grow up.)
Top Network Posts
- 2174Why doesn't GCC optimize a*a*a*a*a*a to (a*a*a)*(a*a*a)?
- 58How to generate all pairs from two vectors in MATLAB using vectorised code?
- 35Is it possible to export constructors for pattern matching, but not for construction, in Haskell Modules?
- 29Where can I learn about #ifdef?
- 25what is the purpose of arrows?
- 15What does `true = false` mean in Coq?
- 12anonymous namespaces and the one definition rule
- View more network posts →