wizeman

52 ms·

391.
by wizeman 9y ago
> A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. Indeed, I agree, but lots of people never ask themselves how much more at r
392.
by wizeman 9y ago
You don't need to go all the way and specify/prove everything in order to achieve significant assurances of absence of (at least certain classes of) bugs. See the section "Use SPARK at the right level for you" [0] for an
393.
by wizeman 9y ago
> sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily. > All that said, automation of provers based on the LCF approach with a non-constructive logic is
394.
by wizeman 9y ago
> Is this true though? What program properties can Isabelle easily automate the proofs of that Coq cannot? Almost all? Granted, I haven't used Coq very much, so correct me if I'm wrong, but isn't it true that in Coq, with
395.
by wizeman 9y ago
That Coq has a stronger logic is an argument I hear often, but is that really so important when the result is that it's so hard to use that no real-world software engineer is ever going to bother? Maybe with HOL I will not be able to p
396.
by wizeman 9y ago
I almost completely disagree with the author of this article. Yes, formally verified systems still have bugs due to the TCB (the trusted computing base). But that's because the TCB is precisely the only part of the system that is not
397.
Prove in the Cloud with SPARK Ada(spark-2014.org)
6 points by wizeman 9y ago|0 comments
398.
by wizeman 9y ago
I especially like the way the following video explains the long-term vision of why Bitcoin is valuable. Once you understand the long-term vision, and how Bitcoin's fate is still very much up-in-the-air in some respects and still subjec
399.
by wizeman 9y ago
I know in the past NixOS did the same for the ZFS kernel module: prior to NixOS installation, it was able to download the ZFS source code, build it and then load it from inside the installer Live CD/USB while it was running, and this w
400.
by wizeman 9y ago
The license incompatibility is on the GPL side, not on the ZFS / closed GPU side. The only ones which could sue are the Linux kernel developers.
401.
by wizeman 9y ago
I'm afraid that's not enough in practise: you will also have to specify (and verify) things like: the implementation does not touch memory except the array to be sorted (and some auxiliary variables). If you don't, it wi
402.
by wizeman 9y ago
You sound like you have more experience in this area than I do, so please correct me if I'm wrong. In the context of the original poster, the size of the specification that matters with respect to being a potential source of errors is
403.
by wizeman 9y ago
It's not true for all cases, but it's true for most real-world cases, especially for typical combinations of specification tools and traditional (imperative) programming languages. A real-world program is usually more complex and
404.
by wizeman 9y ago
It can definitely be done with Coq. The typical recommendation is to read through and do the exercises in the freely-available Software Foundations book [1], which will teach you how to do that in Coq. That said, while it was educational an
405.
by wizeman 9y ago
Are there any modern crypto algorithms that are, by design, immune from an attack such as this? Would not having any key-dependent code paths be sufficient to prevent this attack? If it is possible to be immune by design to power analysis,
406.
by wizeman 10y ago
cjdns works for me and seems quite secure as a private, distributed VPN. It automatically assigns an unforgeable IPv6 address to each node: https://github.com/cjdelisle/cjdns
407.
by wizeman 10y ago
Take a look at dafny [1] and F* [2]. Both are open-source and it appears that both of them are able to prove code to be correct with considerably less proof code than traditional interactive theorem provers (such as Coq or Isabelle), mostly
408.
by wizeman 11y ago
What do you mean, it will never happen? The nix package manager has (admittedly, undocumented) support for Rust / Cargo projects.
409.
by wizeman 11y ago
Well, consensus between whom? How would you do distributed, anyone can participate at any time, byzantine consensus but still prevent Sybil attacks?
410.
by wizeman 11y ago
What if knives had been invented by a drug lord? Who cares? What's important is whether knives are useful to us or not. If the inventor is a drug lord, then the problem is that he is a drug lord, not that he invented knives. If someone
411.
by wizeman 11y ago
Actually, that is not true at all, I don't know why you're saying that. It's quite easy to set up a development environment with the build tools / dependencies you need: https://nixos.org/wiki/Develo
412.
by wizeman 11y ago
Have you tried NixOS? I run the unstable channel, which is updated quite often. Don't be scared of the name "unstable", because it's really quite stable since the channel only updates when all tests pass. Also, it's
413.
by wizeman 11y ago
This is not a book, but could be a starting point: http://www.hsph.harvard.edu/nutritionsource/
414.
by wizeman 11y ago
Efficiency and ease of debugging? Just because it's possible to transpile to JS doesn't mean the resulting code will be fast/responsive or easy to debug. Which in turn means it won't be used for significant projects.
415.
by wizeman 11y ago
It doesn't go all the way down. Obviously, you can't have a society where some people are free to murder other people. But other than ensuring freedom and basic human rights (and perhaps some other minimal rules), why should you h
416.
by wizeman 11y ago
I'm perfectly fine with self-governing and self-ruling, I'm just not fine with a group of people governing and imposing their rules on the others. If you or a group of people want their own currency with their own rules that'
417.
by wizeman 11y ago
No, you're right. Democracy IS the best way to run a currency. Let's run our companies as democracies too, that's certainly a good idea! This way everybody has a say in what Microsoft and Oracle do. Oh wait, that's a ter
418.
by wizeman 11y ago
> Something that could potentially govern people's lives (i.e. a new kind of currency) that they have no say at all in operating? Aren't you talking about the USD here? How do you have any say at all in what the Federal Reser
419.
by wizeman 12y ago
Luckily, it seems that Rust code is starting to get integrated into Firefox: https://twitter.com/indygreg/status/570010688027959297
420.
by wizeman 13y ago
Given that the axis in question represents genome size, I'd guess "bp" stands for "base pairs", not a billion units of something...

More ›