Even though I have always seemed to fall back to Vim in a terminal for my coding, I have been using Atom (with SSHFS) for some time now and for reasons I don’t quite understand yet, I’ve not really felt the urge to stop. My initial impressions were that Atom is a Sublime knock-off with some more flexibility, so I expected after a short time of playing with my invite, to go back to my tried and true Vim since that’s what I did with Sublime. But here I am, and I’m more convinced to stick with it some more now that it has been open sourced. The ‘gq’ wrap lines feature was one I sorely missed, so I thought I’d try to script it.
I was surprised at how easy and quick it was to code a package for it, and to subsequently make available to everyone else through their package management system (the image above takes you to the package). On a slightly related note, my friend Rob pointed me to this interesting Vim modernization project.
More specifically, he suggests some of the ‘thought’ before coding should be formalized as a specification (like a blueprint) written in the language of mathematics. The TLA specification language uses satisfiability of boolean formulas as a mathematical way to express initial states and the possibilities for a state to transition to other states. The framework provides the programmer a way to (1) think in depth about the possible states before coding and running test cases, (2) better document what an implemented piece of code does making it more convenient for updates later, and (3) automatically find bugs from logical inconsistencies.
This video provides more motivation and examples for what I said above, including a couple of anecdotes that mentioning the use of TLA by Amazon and Microsoft. Overall, I think he made a good argument that putting more effort in the specification can lead to better design decisions down the line.
A couple of notes:
(1) This approach is mostly about ‘functional’ specification, so it provides little assistance in implementing such a specification. In this way, it is largely independent of programming language choice/design, compilation, and optimization in practice. Many specific algorithms could satisfy a functional specification. In his talk, I got the impression that these other issues were trivial in comparison to specification, which I don’t think is often the case. However, I certainly agree that more thought should be spent at the specification stage, if possible.
(2) Large-scale adoption of this formalism seems like it would be difficult. There is the obvious overhead in teaching people to understand and implement this formalism in their work. Even if knowledge of TLA was part of a programmer’s toolkit, this type of formalism may be far more beneficial for specific, more ‘predictable’ problems. By predictable, I mean that a programmer (or computer) can consider the possibilities of desirable and undesirable states a priori. For example, the task “write a program to produce a pleasing sound” is not only a larger/more general problem, but it also very difficult to specify it exactly. This is an extreme example, but less extreme versions of it are a very common and practical form of programming (e.g. programs that are highly dependent on human satisfaction during use). For these applications, past intuition, seeing how you, a test group of people, and even your customers respond to your program may provide the most valuable information for improvement.
Leslie Lamport is a computer scientist working at Microsoft Research. He recently won the Turing Award (one of the highest honors in computer science), and ever since I learned about Lamport clocks, he has been one of my favorite CS academics.
I have made two new Googly purchases recently. The HP Chromebook 11 and the Nexus 5.
Nexus 5 thoughts soon, but after a few weeks with this Chromebook, I have found that this has effectively replaced my tablet and a surprisingly, many things I do on my Macbook Pro Retina 15”. One of the reasons I wanted to try it out was that I found I often wanted to chat or write a quick email or do some basic keyboard-level content input with the tablet, but didn’t want to pull out a full-fledged computer. This got me interested in the announcements for the Chromebook and the new Microsoft Surface (or potentially a new Macbook Air 11”? That would be very tempting). So for me, while the Chromebook is more of a notebook than it is a tablet, I find that I use it more like a tablet: to quickly look up and input content.
Pros in my experience:
- Surprisingly, this is currently my most used device. My Macbook Pro Retina 15” is now used almost solely for larger, visually-intensive projects like creating a presentation or poster. And my tablets have become fancy remote controls lately.
- Super inexpensive
- Incredibly handy: can fit a tiny netbook/tablet bag
- Great for content input vs. a tablet
- Micro USB charging very handy: don’t have to carry two chargers
- Display is really good (this is what got me interested in the first place): very nice contrast and viewing angles (even when compared to the Macbook Air)
- Font size scaling in Chrome is nice: iPad + keyboard, for example, doesn’t scale fonts well, so it’s hard to use when placed at a distance: i.e. towards your lap or knee vs. held up near your face. Chrome on a Macbook Air can scale fonts, but that’ll run you about $1,000: and you’ll have a less appealing display at the moment.
- Very light: can easily hold it in one hand
- Nice to use for coding via SSH
- Can be laggy/frame-droppy at times: especially when compared to a Chromebook Pixel, Mac or Google/Apple tablet experience. For a similar price, I believe the Asus and Samsung models may be faster, but the displays aren’t as appealing.
- Native apps like Hangouts or Keep don’t appear to support font size adjustment. I just use the browser instead.
- If you were to use this for presentations, I’m not sure how you would give one.
- Low battery life.
For the price, those are the only cons I can think of after weeks of use. This Chromebook may not have been targeted to a geek like me who already has much more powerful, beautiful machines, but it certainly has won me over. Things I’d like to see in the next iteration of entry-level Chromebooks by Google:
- Smoother. Please make this a smoother, more responsive laptop! Maybe the Asus or Samsung models are smoother, but I really liked the display on this one. I think many would pay the premium for this. One of the things I like about Apple products is that no matter what ‘line’ you get from them, you typically don’t experience any major lag in performance for basic tasks, and I think this is a good standard for Google devices.
- Ramp up native Chrome apps to be more like a nice tablet experience. For example, make a native Youtube or Gmail App that immerses you in.
- Maybe a touchscreen like a lot of Windows models are going with (or the new Acer C720P!)?
Want an individual color from a color map in matplotlib? You would think this would be easy (and it is as you will see below), but as I traversed the documentation, I could not find for the life of me how to do this. After looking at various matplotlib functions, Rob and I finally found that it’s really simple (and apparently undocumented as far as we can tell). Just choose your colormap (e.g. ‘jet’) and call it like a function with a value between 0 and 1: e.g. pylab.cm.jet(.5). This will return you the rgba 4-tuple that you can use for whatever.