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
- 1975Why doesn't GCC optimize a*a*a*a*a*a to (a*a*a)*(a*a*a)?
- 50How to generate all pairs from two vectors in MATLAB using vectorised code?
- 34Is it possible to export constructors for pattern matching, but not for construction, in Haskell Modules?
- 27Where can I learn about #ifdef?
- 23what is the purpose of arrows?
- 13What does `true = false` mean in Coq?
- 12anonymous namespaces and the one definition rule
- View more network posts →