Most of what I do are affected by the tools I use. In writing math my two options are paper and LaTeX. I am a total slob when it comes to paper: loose paper are all over the place and my notebooks are like a homeless graphomaniac’s ramblings. That leaves typing in LaTeX, and when it comes to editors I am an editor-agnostic: I’ll do emacs, vi, nano, gedit or even ed. If you observe me long enough, you can even see me doing straight cat into a file.
When it comes to programming, I am IDE-averse. Apart from emacs, the last IDE I used was probably Turbo C back in 90’s. Because, if my IDE’s raison d'etre is to do the boring stuff for me, may be I am using a wrong language to start with. You don’t want me to pull a Kant on you:
If I have a book that thinks for me, a pastor who acts as my conscience, a physician who prescribes my diet, and so on–then I have no need to exert myself.
True tools are languages. Editors and frameworks are conveniences.
George Perec once wrote a whole novel on a type-writer whose e-key was removed which was in part inspired by another novel written by an obscure American writer Ernest Wright. In the same vein, if I’d like to write programs that severely restricts my use of side effects then I’d use haskell. If I’d want to do this on the JVM platform then I’d switch to frege, probably. Different objectives and constraints require different tools, and in turn, these constraints might bring out novel ideas you wouldn’t normally think of.
In short, learn as much as you can and as diversely as you can. Make choices and write, or cat if appropriate.
Idris has been on my todo list for a long time. A strongly and dependently typed functional programming language similar to haskell. I am mainly interested in idris’ interactive theorem proving capabilities.
I know that coq is the de facto standard and it does a more comprehensive job than idris, but I like its haskell-like syntax. If you are interested, check Homotopy Type Theory, a machine assisted proof of Feit-Thompson Odd Order Theorem in coq, and a coq proof of the Four Color Theorem.
There are many old, and new and experimental formal proof assistants out there. Here are a few in case you’d want to check out:
Every journey starts with few small steps. So, here are mine: I am going to verify that the addition in the set of natural numbers is commutative. This proof is different than the commutativity proof given in the official documentation of idris.
The set of natural numbers is given as a recursive type which as a
bottom element Z and recursively defined as
data Nat = Z | S Nat Unlike haskell, the type definitions are preceeded by :
instead of :: as you can see below:
unit: (a: Nat) -> plus a Z = a
unit Z = Refl
unit (S k) = rewrite unit k in ReflMy first lemma is the unitality of the addition. The proof is a
simple recursion/induction argument. I think of Refl as the
bottom type in proofs which is x=x reflexivity: if you can
reduce your proof to that you are done.
The next lemma is the about the fact that (n+1)+m=n+(m+1).
unloop: (a: Nat) -> (b: Nat) -> plus a (S b) = S (plus a b)
unloop Z b = Refl
unloop (S k) b = rewrite unloop k b in ReflThen the rest is recursion on the second argument:
comm: (a: Nat) -> (b: Nat) -> plus a b = plus b a
comm Z b = rewrite unit b in Refl
comm (S k) b = rewrite comm k b in rewrite unloop b k in Refl