search

mit-pdos / fscq

FSCQ is a certified file system written and proven in Coq
Other
236 stars 21 forks source link

Hard link support #8

Open dsheets opened 9 years ago

dsheets commented 9 years ago

Some applications depend on file system support for hard links.

zeldovich commented 9 years ago

I think hard links are a bad idea in the context of fscq. Hard links make the spec much more complicated (i.e., the file system state cannot be thought of purely as a tree). Worse yet, a spec that supports hard links makes it difficult to write certified applications on top of fscq, because the application cannot rely on a simple tree view of a file system (e.g., that two paths in the tree refer to distinct files, that changing one part of a tree doesn't change any other parts of a tree, etc). So, I doubt we'll add support for hard links.