opnitro

Do you have a link?

I think the "do the normal" thing is very easy to say and very hard to do in general. Should every case of `a / b` inject a `(b != 0) && ((a != INT_MAX && b != -1))`? If that evaluates to `true` then what should the program do? Or: should the compiler assume this can't happen. Languages with rich runtimes get around this by having an agreed upon way to signal errors, at the expense of runtime checking. An example directly stolen from the linked blog post:

  int stupid (int a) {
    return (a+1) > a;
  }

What should the compiler emit for this? Should it check for overflow, or should it emit the asm equivalent of `return 1`? If your answer is check for overflow: then should the compiler be forced to check for overflow every time it increments an integer in a for loop? If your answer is don't check: then how do you explain this function behaving completely weird in the overflow case? The point I'm trying to get at is that "do the obvious thing" is completely dependent on context.

Different user, but sure! Three examples:

1) you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized. So you want to state that they always produce the same thing.

  fn my_complex_algo(x : Input) -> o:Output ensures o == simple_algo(x)

2. You might have high level "properties" you want to be true about your program. For example, a classic property about type-checkers is that they are "sound" (meaning that if you say a program is well typed, then when you run it it must be impossible to get a type error).

3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.

Lot's of great work on dafny in general!

ya got me

Nit picking, but floating point is commutative either.

  1 + NaN == NaN
  Nan + 1 == NaN
  Nan != Nan

(NaN is defined as not being equal to itself)

As a huge believer in formal methods, this statement should _also_ be tempered somewhat. Formal proof is a great technique, but it's incredibly dependent on getting your specs right, which is very hard to do.

As an example, CompCERT is a formally verified C compiler, and it's had a couple bugs as a result of their specification of the underlying hardware being wrong.

Sure, wasn't meant as a slight in any way. For certain use cases, that's a great set of defaults! It's very good to have an OS that makes those choices. Needing to explicitly opting into things that raise your exposed attack surface is really really nice!

I'm guessing it's a reference to Go

This is a _very_ qualified statement. The default OpenBSD install enables an extremely small amount of services by default, which is why they can claim that. I'm not saying that's wrong, or a bad idea, but obviously a platform that doesn't enable many network services is going to have a small amount of remote holes.

this is on top of a lot of very careful programming and interesting security research, and this post isn't meant to take anything away from the OpenBSD devs.