I think it's a good thing for this sort of service to come out now while Bitcoin is fairly young. Accepting zero-confirmation transactions has always been bad practice, making double spending more likely in this case means that people will be far less likely to accept them.
A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ for it though.
The challenge comes in when you try to translate. You write your model up and validate your approach, you then try to translate it into C (or whatever) and that point you can be as certain of your design as you like, you still can't be sure that the compiled software will work properly. I haven't seen a convincing solution to that particular problem (and I've done some research on the topic for three separate projects now).
I have just recently started using the excellent Hacker News 2 app so if you're on Android, you might give it a try. It scrapes the page so it's almost like a mobile version of HN. It's also open source and regularly updated.
It amazes me that legal costs aren't going to be definitely paid here. That alone makes this system almost impossible to appeal, pro-bono lawyers aren't likely to work on this issue after the first one or two high profile cases if there isn't a payout.
The problem here is that the conduct that led to the lawsuit must be intentional and exceptional in order for a court to be able to award attorney fees. While our laws made this an incredibly difficult situation to resolve, the conduct in this case consisted of a simple mistake made on a form by an FBI agent. Unfortunately, that was neither intentional nor exceptional, and thus doesn't meet the standard for a court to award attorney fees.
Surely the conduct should also include the government's egregious behavior during the case?
If in a regular civil suit, one of the parties spent several years lying and making shit up and had absolutely zero case when all was said and done, surely the judge would take whatever opportunity was available to penalize that party and make whole the other party?
The "simple mistake" was not the "intentional and exceptional" bad conduct here. The intentional and exceptional conduct was in not having a clear, transparent, and straightforward process for a person to find out they're on the list, find out exactly why, and appeal.
This is hypocritical. Any other defendent found to have committed what amounts to gross professional negligence that deprived someone of a basic right (freedom to move about) would be looking at some combination of (1) a revoked license, (2) severe damages, and (3) paying the harmed party's legal fees. The longer the US government continues this kind of hypocrisy the more it risks being replaced.
I haven't been following the case closely, but the consensus (even in the view of the plaintiff and the judge) is that the agent misinterpreted the instructions for completing the form, which led to him marking the wrong box on it.
People aren't complaining about the mistake itself, but about the US government requiring Ibrahim to spent 8 years and $3.5 million dollars to correct the mistake. They could have done a review when the lawsuit was filed, and they could have agreed to settle the lawsuit after the mistake came to light during depositions. As far as we know, they didn't do either of those. That's what the gp is implying might be exceptional and worthy of awarding fees.
I can believe that a lawyer working on someone's case for 8 years can credit enough hours to build up to $3.5MM, that's reasonable.
I'm sure she (lawyer) won't let it go easily, as nobody should work for free, for 1 day, or 8 years. The good hope is that eventually couple years from now her bill will be kicked through different departments and different manager's hands, enough times that at some point someone will cut her a check. It may be settled for $1MM or something, but eventually I don't see why she shouldn't get paid and some judge sooner or later will rule some sense into it. Bad news is that she will get paid from mine and yours pocket. Hopefully, this will learn FBI something, but honestly I highly doubt it....
I did some work for my third year dissertation on performing exhaustive testing on floats. Worked well enough, but I was never convinced that it was an especially effective way of testing.
If your test oracle is code itself, then it's not unlikely you'll make the same bug twice. I can't find the paper I'm after, but NASA did some work here.
If your test oracle isn't code, you have the problem of working out the correct outputs for the entire function space (at which point maybe you'd be better off with some kind of look-up table anyway)
The next problem is your input combinations grow much faster than you are able to test. Most functions don't just work on one float (which is very feasible) but they might work on three or four streams of input, and keep internal state.
The moment you have these combinations you run into massive problems of test execution time, even if you can parallelise really well.