wizeman

45 ms·

361.
by wizeman 6y ago
From what you're quoting and from what you're saying, it seems that Bosque (the core compute language) can indeed receive input from the outside world, even though it comes from the runtime (which Bosque considers the outside worl
362.
by wizeman 6y ago
Sure, but they are not simply saying that they do not allow unbounded loops, that is what some languages do already, like Coq. They are saying that the compiled program "uses constant stack space, eliminating any possible out-of-stack
363.
by wizeman 6y ago
> As a result of these design choices there is always a single unique and canonical result for any Bosque program. This means that developers will never see intermittent production failures or flaky unit-tests! So Bosque programs are not
364.
by wizeman 6y ago
Not the OP, but I enjoy playing R6 with bots more than with other people. However, unlike CSGO, R6 doesn't allow you to team up with bots and that makes it a lot more boring.
365.
by wizeman 6y ago
I'm sorry but I don't follow. If you take the Bell test experiment where Alice and Bob perform their measurements at approximately the same time but very far apart, I think you and I both agree that when Alice does a measurement a
366.
by wizeman 6y ago
I think you can make an argument for viewing it that way, depending on exactly what you mean by "you". But IIUC, one of the remarkable things about MWI is that it would be a local hidden variable theory! This is a very important
367.
by wizeman 6y ago
Perhaps you can try the following article, as it was the simplest and clearest explanation I've found anywhere: https://www.physics.wisc.edu/undergrads/courses/spring2016/4... AFAICS it was published in
368.
by wizeman 7y ago
As far as I understand this has been done more than 15 years ago by the "Mines Perfect" game [0], which is open source IIRC. In this case you'd use the Lucky Mode and the Murphy's Law option (although more modes are avai
369.
by wizeman 7y ago
I think the story implies that the attacker didn't survive, since it doesn't say anything about him being sentenced. It was the attacker's cousin (who enlisted him to to perform the attack) that was sentenced. Edit: a comment
370.
SWAPGS Vulnerability in Modern CPUs Fixed in Windows, Linux, ChromeOS(bleepingcomputer.com)
3 points by wizeman 7y ago|0 comments
371.
by wizeman 7y ago
Doesn't the GDPR also apply to entities that process personal data (as opposed to only those that store it)? AFAIK it should apply to entities that share personal data with third parties, for instance.
372.
JetBlue explains to a passenger how it got a photo of her face(boingboing.net)
409 points by wizeman 7y ago|229 comments
373.
by wizeman 7y ago
We know there is life in the universe (on our planet), there is empirical proof of that. So the question now is whether there is also life on other planets. If you don't think there is life on other planets then you must think our pl
374.
by wizeman 7y ago
Humans have historically had an inherent bias in thinking that we as a species and everything around us is somehow special, only to later discover that it was never true all along. For example, for a long time we've thought that we are
375.
by wizeman 8y ago
It doesn't discard the oldest item, it discards the item that was least recently used/accessed (LRU, like the name says). To see the difference more clearly, note that the oldest item can in fact be the most recently used one.
376.
by wizeman 8y ago
I still don't understand why you are mentioning legal tender in this discussion. Legal tender is cash, credit cards are not legal tender. Therefore Amazon does not accept legal tender. Yes, businesses like Amazon could demand payment i
377.
by wizeman 8y ago
I don't think "legal tender" means what you think it means. In many jurisdictions (including the US and the Eurozone, as far as I know), almost no business is required to accept legal tender as payment. Legal tender is only r
378.
by wizeman 8y ago
> If I'm understanding this correctly, you want to do something like this: Exactly! > But Why3 does not support this? As far as I can tell, it doesn't. I get a syntax error if I either try to name the argument to pred or if
379.
by wizeman 8y ago
> What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_sear
380.
by wizeman 8y ago
> Can something like that work? Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works. Therefore, I hereby declare that you
381.
by wizeman 8y ago
Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor cave
382.
by wizeman 8y ago
Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try t
383.
by wizeman 8y ago
Actually, I can definitely say that this version is not broken, i.e. I've formally proven it to be mathematically correct assuming that: 1. high and low are bigints (such as when using Python, for example) 2. the input array is sorted
384.
by wizeman 8y ago
I'm very far from being an expert, but as far as I understood the reasoning, it seems that the author is arguing that as time passes, the current conditions of chaotic physical systems are going to start depending on more and more info
385.
by wizeman 9y ago
You're right, thanks! It was an unfortunate typo.
386.
by wizeman 9y ago
Why are you dividing by 3600? The numerator is already in kWh units (kW hours), it's not kW seconds.
387.
by wizeman 9y ago
How did you go from 2,079,720,000 KWHrs to 24.07 MW of electricity, 24/7? My calculator and Google (search for "2079720000 kWh per 24 hours to MW") says it's more than 86,000 MW (so ~86 GW). edit: corrected units from TW
388.
by wizeman 9y ago
> Coq's been around since 1989. Maybe those 28 years have something to do with it. Isabelle has been around since 1986, so that alone doesn't explain it.
389.
by wizeman 9y ago
See [1] for an example (edit: although this may not be the best example nowadays, see below): Quoting: > Consider the conjecture "length(tl xs) <= length xs", which states that the length of a list’s tail (its "cdr&quot
390.
by wizeman 9y ago
> I definitely wouldn't want to spend time proving correctness of every single line of code I write; it would make programming "no fun" zone and require rocket-science level of understanding. Fortunately, you don't ha

More ›