hacker-school-wednesday-june-11-2014

Tahoe-LAFS symlinks:

• I read through the test I'd like to modify: https://github.com/tahoe-lafs/tahoe-lafs/blob/master/src/allmydata/test/test_cli.py#L2805

  • I noticed a couple of instances of hard-coded constants in the test code. I might like to suggest some patches to those, but I didn't want to depth-first at this point. So I simply made a note of them.

  • Understanding the test involved understanding Twisted callbacks. I asked for help on the local chat and on #tahoe-lafs to make sure I was reading it right.

  • I did succeed in fully understanding the test! I started working out how to replace it.

    • This prompted a discussion on #tahoe-lafs about whether symlinks should be followed in the backup call. The issue is that now if a restore is attempted, multiple copies of the same file, which converge in the Tahoe-LAFS system, will become copies in the restored system. I had already been aware of this problem, but based on the notion that restore is not a solved problem in Tahoe-LAFS (there is no such inverse command, there are only cp and get), I had decided that this could be dealt with later. However, there were some worries about whether supporting symlinks for backup should entail creating metadata to support symlinks on the Tahoe-LAFS side.

    • I used this opportunity to refresh my understanding of the difference between symbolic links and hard links. Basically, symlinks have an extra layer of indirection, but a hard link is just another reference to the file/directory inode. When you type ls -l the second column is a count of existing references to the file or directory including the one being listed. Hard links add to this count, but symlinks don't. Hard links to directories are considered dangerous. I don't yet know why.

      In other words, a hard link is indistinguishable from the original. In fact, once there is a new hard link, there is no longer a meaningful notion of original.

      This in turn made me rethink my motivation for the patch in the first place! The tagging program I want to write will work just as well with hard links as with symlinks. The only thing I can think of that would be more work, is if you want to delete a file from your filesystem, you have to find all the references to it and delete them all. (I wonder what the Rust perspective would be on this. Hard links are borrowed references in a sense, and there should be only one copy in use at a time.) Otherwise, I can't think of any reason to use symlinks. Maybe someone could try to persuade me they are useful.

      As to the patch, I could still write it. Given that people who use Tahoe-LAFS probably have existing symlinks, it could still be useful.

      I plan to chat with the devs more tomorrow.

Working with others

• Paired a bit with another person going through the Factor tutorial.

• Joined the Project Euler group. We all decided to learn Haskell thereby. The second question requires writing Fibonnaci, and so I had to re-relearn tail recursion. I think that's in the first chapter of SICP. That reminds me that I was considering going though SICP and solving the problems in Haskell. Or Factor. Heh.

• Alan gave a tutorial on Coq. Here are my notes:

  • all proofs are on construction by induction: intuitionist, no law of excluded middle!

  • things that don't prove don't compile

  • not turing complete?!

  • Curry Howard correspondence makes a analogy:

    types <--> propositions

    terms <--> proofs

    • To prove: construct a term/value whose type is the proposition
    • expressions evaluate to types or propositions
    • If the compiler says that the term type-checks to the proposition, then the term is a proof of that proposition.

    • Presumably, if the implementation of an algorithm in eg. Haskell, is isomorphic to a proof in Coq, then this is a proof of correctness of the implementation.
    • tactics is a tool that helps writing proofs.

    Although Alan talked about how Coq is a gentle way for programmers to learn math, it also seemed like a great way for a mathematician to understand the power of type systems. I was really blown away.

Reading

Didn't get to the Monads.