The program defines a type `t` with 257 constructors (`C_0` through to `C_256`). As an analogy, the type `boolean` has two constructors (`true` and `false`).
Each of these constructors takes a natural number as an argument.
It then defines a function `is_256` which checks whether it's argument has the form `C_256 n` for some `n`, returning a boolean.
It then defines the value `falso` of type `False` (which shouldn't be possible). It does this by defining two values: one has type `is_256 (C_256 0) = true`, the other has type `is_256 (C_256 0) = false`. This is clearly a contradiction, which is used to construct the value `falso`.
The reason one value gives `true` and the other `false` is that the former is getting calculated by the regular Coq implementation, whilst the latter is getting calculated by the buggy `vm_compute` alternative. vm_compute should give identical results, but faster; but since there's a bug, we can derive a contradiction by mixing correctly-calculated values with incorrectly-calculated values.
It's like the opposite of && (continue until one alternative is false), for if you want to continue with alternatives in sequence until one alternative becomes true: a || b || c || ...
This usage is commonly found in other places than the shell, like JavaScript, Perl, and PHP.
Thanks, I know `||` in general--I meant I hadn't seen the specific construction GP had used. The error handling to delete the output file in case the command failed is really elegant.
>Fun fact: ASCII actually reserved control characters for this stuff. 1F is the "unit separator" and 1E is the "record separator". There is even a "group separator" (1D) and a "file separator" (1C).
Which means you can't safely use it for arbitrary data (since your records themselves could contain these separators). Most of the time that doesn't matter; sometimes it does.
Why not have Apple require apps to run usefully with just basic permissions? Anything beyond access to own files is optional. This could certainly be gamed, but scrupulous app authors could gain a ton of trust from playing ball.
This is essentially already the case as Mac App Store apps must be sandboxed. This works fine for a lot of apps, but has presented issues for many prominent developers. (e.g. Panic had a fairly difficult time adapting Coda to the sandbox, if I recall correctly.)
Oh yeah having six or more horizontal navigation bars was pure pain. Considering how difficult is to effect changes with an established user base, plus the complexity of the domain itself, their new design is anything but cosmetic.
In about a year of using Campfire, I never saw a single bug fix or new feature. We've since moved to HipChat, and while it's not perfect, it's so refreshing to pay for a service that gets regular updates (not to mention has decent mobile clients).
Rollback is essentially like a fork to the past. It creates a new database, but only replays transactions up to a specific instant. It's based on the Postgres Point-in-Time Recovery feature: http://www.postgresql.org/docs/current/static/continuous-arc...
