(https://blog.brownplt.org/img/favicon.png) (RSS) (/feed.xml) Sharing is Scaring: Why is Cloud File-Sharing Hard?  The Brown PLT Blog (https://blog.brownplt.org)    (https://blog.brownplt.org/feed.xml) RSS   (https://cs.brown.edu/~sk/Contact/) CONTACT   (https://cs.brown.edu/research/plt/) GROUP PAGE   PREVIOUS POSTS  (https://blog.brownplt.org/2025/08/25/cloud-sharing.html) Sharing is Scaring: Why is Cloud File-Sharing Hard?  (https://blog.brownplt.org/2025/08/03/paralegal.html) Practical Static Analysis for Privacy Bugs  (https://blog.brownplt.org/2025/06/09/copeanddrag.html) Lightweight Diagramming for Lightweight Formal Methods  (https://blog.brownplt.org/2025/04/29/argus.html) Argus: Interactively Debugging Rust trait Errors  (https://blog.brownplt.org/2024/08/08/ltltutor.html) LTL Tutor  (https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html) Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic  (https://blog.brownplt.org/2024/07/05/plan-feedback-llms.html) Iterative Student Program Planning using Transformer-Driven Feedback  (https://blog.brownplt.org/2024/06/27/differential-analysis.html) Differential Analysis: A Summary  (https://blog.brownplt.org/2024/04/21/forge.html) Forge: A Tool to Teach Formal Methods  (https://blog.brownplt.org/2024/04/12/behavior-misconceptions.html) Finding and Fixing Standard Misconceptions About Program Behavior  (https://blog.brownplt.org/2024/02/02/privacy-telemetry.html) Privacy-Respecting Type Error Telemetry at Scale  (https://blog.brownplt.org/2024/02/01/ppll.html) Profiling Programming Language Learning  (https://blog.brownplt.org/2024/01/01/examplar.html) The Examplar Project: A Summary  (https://blog.brownplt.org/2023/12/28/document-calculus.html) A Core Calculus for Documents  (https://blog.brownplt.org/2023/12/27/plan-notations.html) Observations on the Design of Program Planning Notations for Students  (https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html) Conceptual Mutation Testing  (https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html) Generating Programs Trivially: Student Use of Large Language Models  (https://blog.brownplt.org/2023/09/17/rust-ownership.html) A Grounded Conceptual Model for Ownership Types in Rust  (https://blog.brownplt.org/2023/07/16/second-lang-fun.html) What Happens When Students Switch (Functional) Languages  (https://blog.brownplt.org/2023/02/06/typed-untyped-comparison.html) Typed-Untyped Interactions: A Comparative Analysis  (https://blog.brownplt.org/2022/11/05/little-tricky-logics.html) Little Tricky Logics  (https://blog.brownplt.org/2022/10/15/problem-misconceptions.html) Identifying Problem Misconceptions  (https://blog.brownplt.org/2022/10/10/performance-preconceptions.html) Performance Preconceptions  (https://blog.brownplt.org/2022/08/16/struct-pipe-comp.html) Structural Versus Pipeline Composition of Higher-Order Functions  (https://blog.brownplt.org/2022/07/09/plan-comp-hof.html) Plan Composition Using Higher-Order Functions  (https://blog.brownplt.org/2022/07/07/stacks-dont-stack-up.html) Towards a Notional Machine for Runtime Stacks and Scope  (https://blog.brownplt.org/2022/06/28/static-python.html) Gradual Soundness: Lessons from Static Python  (https://blog.brownplt.org/2022/04/26/pos-val-neg-info.html) Applying Cognitive Principles to Model-Finding Output  (https://blog.brownplt.org/2021/11/24/pbt-revisited.html) Automated, Targeted Testing of Property-Based Testing Predicates  (https://blog.brownplt.org/2021/11/21/b2t2.html) A Benchmark for Tabular Types  (https://blog.brownplt.org/2021/10/02/examplar-weaknesses.html) Student Help-Seeking for (Un)Specified Behaviors  (https://blog.brownplt.org/2021/08/22/codap-transformers.html) Adding Function Transformers to CODAP  (https://blog.brownplt.org/2021/07/31/behavioral-hof.html) Developing Behavioral Concepts of Higher-Order Functions  (https://blog.brownplt.org/2021/07/18/early-adversarial.html) Adversarial Thinking Early in Post-Secondary Education  (https://blog.brownplt.org/2021/01/10/property-based-testing.html) Teaching and Assessing Property-Based Testing  (https://blog.brownplt.org/2020/10/20/examplar.html) Students Testing Without Coercion  (https://blog.brownplt.org/2020/06/27/data-org.html) Using Design Alternatives to Learn About Data Organizations  (https://blog.brownplt.org/2020/05/20/office-hours.html) What Help Do Students Seek in TA Office Hours?  (https://blog.brownplt.org/2020/01/11/examplar.html) Combating Misconceptions by Encouraging Example-Writing  (https://blog.brownplt.org/2018/07/26/perils-of-automated-assessment.html) The Hidden Perils of Automated Assessment  (https://blog.brownplt.org/2018/07/05/mystery-languages.html) Mystery Languages  (https://blog.brownplt.org/2018/06/19/resugaring-type-rules.html) Resugaring Type Rules  (https://blog.brownplt.org/2018/06/11/philogenic-colors.html) Picking Colors for Pyret Error Messages  (https://blog.brownplt.org/2017/07/06/crowd-pl-design.html) Can We Crowdsource Language Design?  (https://blog.brownplt.org/2017/07/03/fmtools-use-crowd.html) Crowdsourcing User Studies for Formal Methods  (https://blog.brownplt.org/2017/07/01/fmtools-usability.html) User Studies of Principled Model Finder Output  (https://blog.brownplt.org/2017/06/20/scope-inference-hygiene.html) A Third Perspective on Hygiene  (https://blog.brownplt.org/2017/06/12/scope-inference.html) Scope Inference, a.k.a. Resugaring Scope Rules  (https://blog.brownplt.org/2017/02/21/permission-store.html) The PerMission Store  (https://blog.brownplt.org/2017/01/25/permission-app-classification.html) Examining the Privacy Decisions Facing Users  (https://blog.brownplt.org/2016/06/26/why-pyret.html) The Pyret Programming Language: Why Pyret?  (https://blog.brownplt.org/2016/02/06/resugaring.html) Resugaring Evaluation Sequences  (https://blog.brownplt.org/2016/01/08/slimming-languages.html) Slimming Languages by Reducing Sugar  (https://blog.brownplt.org/2016/01/02/ifpr-idea.html) In-flow Peer Review: An Overview  (https://blog.brownplt.org/2015/06/02/flowlog5.html) Tierless Programming for SDNs: Differential Analysis  (https://blog.brownplt.org/2015/04/17/flowlog4.html) Tierless Programming for SDNs: Verification  (https://blog.brownplt.org/2015/04/13/flowlog3.html) Tierless Programming for SDNs: Optimality  (https://blog.brownplt.org/2015/03/01/flowlog2.html) Tierless Programming for SDNs: Events  (https://blog.brownplt.org/2014/09/30/flowlog1.html) Tierless Programming for Software-Defined Networks  (https://blog.brownplt.org/2014/06/14/sleep-habits.html) CS Student Work/Sleep Habits Revealed As Possibly Dangerously Normal  (https://blog.brownplt.org/2014/04/01/var-vs-yar.html) Parley: User Studies for Syntax Design  (https://blog.brownplt.org/2014/01/17/typechecking-jquery.html) Typechecking Uses of the jQuery Language  (https://blog.brownplt.org/2013/08/19/incognito.html) Verifying Extensions' Compliance with Firefox's Private Browsing Mode  (https://blog.brownplt.org/2013/06/18/moocs-for-research.html) From MOOC Students to Researchers  (https://blog.brownplt.org/2013/05/31/app-permssions-conclusion.html) Social Ratings of Application Permissions (Part 4: The Goal)  (https://blog.brownplt.org/2013/05/29/app-permissions-weather.html) Social Ratings of Application Permissions (Part 3: Permissions Within a Domain)  (https://blog.brownplt.org/2013/05/22/app-permssions-branding.html) Social Ratings of Application Permissions (Part 2: The Effect of Branding)  (https://blog.brownplt.org/2013/05/18/app-permissions-intro.html) Social Ratings of Application Permissions (Part 1: Some Basic Conditions)  (https://blog.brownplt.org/2013/05/13/aluminum.html) Aluminum: Principled Scenario Exploration Through Minimality  (https://blog.brownplt.org/2013/04/10/private-browsing-changes.html) A Privacy-Affecting Change in Firefox 20  (https://blog.brownplt.org/2013/04/01/moor.html) The New MOOR's Law  (https://blog.brownplt.org/2013/02/19/teaching-gc.html) Essentials of Garbage Collection  (https://blog.brownplt.org/2012/12/10/subtyping-first-class-field-names.html) (Sub)Typing First Class Field Names  (https://blog.brownplt.org/2012/12/03/typing-first-class-field-names.html) Typing First Class Field Names  (https://blog.brownplt.org/2012/10/21/js-eval.html) S5: Engineering Eval  (https://blog.brownplt.org/2012/09/01/progressive-types.html) Progressive Types  (https://blog.brownplt.org/2012/07/17/domevents.html) Modeling DOM Events  (https://blog.brownplt.org/2012/06/04/lambdajs-coq.html) Mechanized LambdaJS  (https://blog.brownplt.org/2012/04/01/ecma-lambdajs-announcement.html) ECMA Announces Official λJS Adoption  (https://blog.brownplt.org/2012/02/28/scripting-objects.html) Objects in Scripting Languages  (https://blog.brownplt.org/2012/01/31/s5-wat.html) S5: Wat?  (https://blog.brownplt.org/2011/12/18/resume-belay.html) Belay Lessons: Smarter Web Programming  (https://blog.brownplt.org/2011/12/11/getters-and-setters.html) S5: Semantics for Accessors  (https://blog.brownplt.org/2011/11/11/s5-javascript-semantics.html) S5: A Semantics for Today's JavaScript  (https://blog.brownplt.org/2011/09/29/js-essence.html) The Essence of JavaScript  (https://blog.brownplt.org/2011/09/13/adsafety.html) ADsafety     (https://blog.brownplt.org/2025/08/25/cloud-sharing.html) Sharing is Scaring: Why is Cloud File-Sharing Hard?   Posted on 25 August 2025. Here is an actual situation we were asked to help non-technical
computer users with: Alice and Bob want to collaborate on a flyer for a social
event. They are more comfortable with Word than with cloud-based tools
like Google Docs. They have both heard that Dropbox is a good way to
share and jointly edit files.  Alice thus creates a draft of the flyer F on Dropbox. She then
shares F with Bob. Bob makes a change using Word and informs Alice
he has done so. Alice opens F and sees no change. Bob confirms he is
editing a file that is in Dropbox.  They have several baffling rounds
of exchange.  Do you see the problem? No? Here’s the critical question: How did
Alice share F ? Alice dragged the file from the Folder interface into
Google Mail. (Do you see it now?) The problem is that “sharing” means at least two very different things: providing a link to a single shared resource, or making a copy of the resource. Each one is correct for some contexts and wrong for others. Does this sound familiar? To us, it certainly is! It’s the same kind of problem we saw when studying programming misconceptions, work that we have (/2024/04/12/behavior-misconceptions.html) studied in great detail as part of our work on SMoL and the SMoL Tutor. Indeed, in this work, we call this the central analogy : the deep semantic similarity between sharing document links ↔ aliasing, downloading or attaching documents ↔ copying objects, and editing documents ↔ mutation.  We therefore find it especially unsurprising that when you combine mutation with sharing, people get confused. (Of course, there may be a deeper problem: that people are just not very good at reasoning about sharing and mutation. Cloud file-sharing and programming may just be two concrete instantiations of that abstract difficulty, and the same problems may arise in other domains as well.) Essentially, cloud file-sharing operations form an end-user instruction set architecture (EUISA) over which users “program” to achieve their goals. This paper builds on this idea in the following ways: We identify this analogy both in the abstract and through several concrete examples (drawn from personal experience). We use our knowledge of programming semantics misconceptions to design corresponding cloud file-sharing situations, and show that people are confused there also. Drawing on the computing education literature, we devise an interesting way to get crowdsourcing subjects to not only “trace” but also “program” over the EUISA, and show that difficulties extend to both situations. We present a formal semantics for cloud file-sharing. We then discuss how this formal semantics might be employed to help end-users.  For more details, see (https://cs.brown.edu/~sk/Publications/Papers/Published/akf-sharing-scaring/) our paper ! As a fun aside: The formal model is built using (/2024/04/21/forge.html) Forge . We were going to build a custom visualization but, to get a quick prototype in place, we used (/2025/06/09/copeanddrag.html) Cope and Drag . But the CnD spec was so good that we never needed to build that custom visualization!