?

Log in

No account? Create an account
Semiformalishmaybe

Cats with Carrots

Cleaning: almost finished (not very interesting! This is mostly note-to-self)

First I tackled the living room, which took me quite awhile. It still could probably use some more vacuuming and washing of surfaces, but it's fairly tidy and clean, and there are very few things in the room that should either be elsewhere or tossed. Last night, the bedroom got the same treatment - finally tossing out all clothes that are in bad shape (whoa, a lot), things in memory boxen that never should've been in there in the first place (old MP3 players? seriously?), pillows that developed holes some years ago, things I made with yarn a long time ago that didn't hold together, large piles of broken electronics, etc.

End result: Kitchen has Mt. Garbage pairing another peak on my back porch. I want to do a similar purge of my kitchen, but will probably have to wait for garbage day. Also, I hope I don't have too much for the garbagemen to take in one load. On the upside, it feels a bit surreal living someplace this clean and tidy. It's nice that once things are this clean, it's not hard to keep them that way.

Added bonus: I found my awl (so I can make some small improvements to my sandals) and my Kippah (which isn't terribly useful to me, although I'm fond of it).

Anyhow, w00t.

Recently I've been reconsidering a large software project I occasionally bumped into (and disliked) during undergrad - its broad goal was software reusability using contracts between software components. One of the marks of a good abstraction is that it tidies up things that are instinctually worthwhile, and a formal statement of what a function/object/method does is that to the informal documentation we expect of it. Question remains: are contracts the best way to do that? In conjunction with or replacing less-formal descriptions? Are contracts, stated in a predefined language, themselves subject to bitrot as new cross-cutting concerns (reentrant? recursion-safe? discretely separable? aliasing-safe? etc) change the way we think about code? There's obvious goodness when the compiler (or contract-checker) can say "hey, your concepts don't line up right as far as I can tell", and reusing chunks of code is something we all do, which is obviously valuable. How does the formalism line up with the canned message from another expert saying "here's the deal, ...."?

To risk stepping on a few toes, I wonder if they decided to build their language on top of C++ because it's such a messy and conceptually-leaky language that the efforts to engineer-ise it made such a big difference (and the consequences of people getting those efforts slightly wrong when learning were readily apparent).

Also have been thinking about how much trouble it is to move things between the various computing devices I have. It seems like it'd be worthwhile to have proximity handled better by such devices - why can't I effortlessly move running applications between my AndroidPhone and my desktops, toss notes and bookmarks around with just a flick/mousedrag, etc? Things are not terrible on this front (unix has generally been good at letting one run apps elsewhere with GUIs piped around), but I neither want to lose what's there with technology's progression towards convergence (AndroidPhones should be first-class computing devices by this metric) nor am I content with the status quo. To dream about what operating systems look like in the future, their upper layers would be written with this kind of thing strongly in mind. If I notice that I'm using software to move data/files/applications between these devices, the interface is too visible (although it's reasonable for devices that have not chosen to trust my network to pop up a yes/no).

Comments

I handle the move-between-devices problem in a way that is satisfying to me, but perhaps not to others. Everything I care about, I do in text mode, in a screen session, on my server. This includes IRC/AIM/Gtalk, email, and access to my database-of-stuff I will mention in a minute. I access things from my phone or my laptop or my desktop by sshing to my server and joining the screen session.

I keep all the information I care about in a perl-hacked-together database on my server, which is replicated to my laptop. I access it from the replica on the laptop, or by sshing to the server from my phone. This includes my contact list, which is why you will see me dicking around with ssh when I need to look up a contact, rather than using the builtin app. This gives me portability and durability at the expense of usability, which is a tradeoff I'm willing to make.

The one exception to this whole scheme is browser state; my set of open tabs on each device is distinct to that device. I find this annoying and hope that it will not be the case in the future. I'm not actively working towards making it the case at this point, though I have some ideas for how that could be done.
That gets you something, as do other efforts to do this at the application level - pidgin, for example, is theoretically being extended to a client-server model so people can run the backend one place and connect to it from wherever (hopefully that project won't fail). screen is, as you note, a very good thing. I'm not as comfortable centralising around screen - I do a lot of things from a terminal, but not everything. Screen doesn't help you move audio streams or running applications around, even if it's good at what it does.

I think this kind of thing should probably be the job of the higher levels of the OS (thinking broadly about what an OS is in this context - this is probably best handled at levels near that of the Windowing system?). I don't think we should have an entirely separate software stack on AndroidPhones from our desktopis - maybe the lower levels can or should remain different, but a layer on top that would intelligently cluster systems would do the job. I'd start thinking on terms of every machine in an area exposing all its filesystems to the others and have any machine capable of addressing the others screens and other IO devices, and move onward to thinking about how they could ask each other to do things, process migration, and the like (hey application, serialise all your transferrable state because another instance of you is about to pick that stuff up on another system).

Getting a good security model for that is important too.

Doing this would probably involve application programmers changing the way they write software, at least a bit. Hopefully it wouldn't require weird tricks with VMs.
There are various Android apps (and desktop browser plugins) that try to solve the problem of moving data between nearby devices. Astro File Manager, Hoccer, Share By QRCode (and its equivalent Chrome plugin), Dropbox, Chrome To Phone and android2cloud come to mind. Not to mention QuickSSHd, which is what I usually end up using.

But yeah it could certainly be easier. Dropbox is probably the friendliest solution, but it uses an outside server.

contracts

Contracts are not the end-all be-all of software specification, checking, and modularity, but they're a good first step. My experience with them so far in the course we're teaching is that they give you a formal language in which to write down otherwise-tacit invariants you have in mind about your data representations and their various intermediate states. In this way, they making programming dramatically easier (not to mention more fun!), because keeping track of complex invariants in your head is extremely difficult, especially if they may change as you develop the code.

In our toy language, we so far have only dynamic checking of contracts, but that's a lot better than nothing, since it gives you some sense that the things you're writing down are somehow meaningfully and mechanically verified. The problems with (even expert-written) documentation are that (1) no machine is checking that it's up to date, and (2) informal language leaves room for interpretation. If a contract becomes out-of-date, it is likely to be caught quickly by dynamic checking so that whoever made the change knows to update it. More importantly, if a contract is ever violated, dynamic checking tells you precisely the point where human reasoning about the code became out-of-sync with its actual execution.

My admittedly limited experience with them has been unexpectedly positive! Programming with formal contracts can be quite liberating in a way -- it's like being given paper and pencil for the first time when you've been trying to do complex mathematics in your head.

Re: contracts

For philosophical reasons, I don't accept the strong form of verification, but I recognise that "this seems to work so far in catching the errors we know about" is a very useful property (trying to skirt a long philosophy-of-math/logic discussion, for now).

The programming project I recall was .. kind of cumbersome, required people to learn another language, was too low-level to easily express anything conceptual enough (commonly a problem with contract systems - their expressivity doesn't tend to go beyond simple maths and perhaps simple data structures), and was parallel to the actual software framework they were using. Still, I'm coming to think that despite these faults, what they were trying to do is probably worthwhile, and while I don't like being forced to use contracts, I much appreciate the option to use them.

We may have had this conversation before - in programming languages I am a big fan of the presence of optional mechanisms that programmers can use to give hints to the compiler - so long as they're optional and that the compiler can use them to make my code faster, to tell me I probably am doing something stupid, or that I've done something I said I would not, I am very happy. I like the ability to have tools to help me use discipline, but don't like when that discipline is mandatory.

You're right about code/comment drift, but I don't think informal language is necessarily ambiguous (maybe one could prove that if it is not, it can be converted into formal comments?). More importantly, I think often formal language is horrible to read - given a choice between a manpage (or most Java API docs) and a contract, if I only had one I'd skip the contract every time (might be nice to have both just in case the user docs actually are ambiguous, although I generally prefer just to avoid ambiguous areas of a spec).