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.

I think this is a point of view that seems sensible, but probably hasn't really thought through how this works. For example

  some_array[i]

What should the compiler emit here? Should it emit a bounds check? In the event the bounds check fails, what should it do? It is only through the practice of undefined behavior that the compiler can consistently generate code that avoids the bounds check. (We don't need it, because if `i` is out-of-bounds then it's undefined behavior and illegal).

If you think this is bad, then you're arguing against memory unsafe languages in general. A sane position is the one the Rust takes, which is by default, yes indeed you should always generate the bounds check (unless you can prove it always succeeds). But there will likely always be hot inner loops where we need to discharge the bounds checks statically. Ideally that would be done with some kind of formal reasoning support, but the industry is far that atm.

For a more in depth read: https://blog.regehr.org/archives/213

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!

This is why I think interactive proof assistants (as opposed to "automatic" ones like Dafny), are a better starting point for learning. You're still gonna need to learn some higher level concepts, but you won't have the frustrating experience of the automation just failing and leaving you shrugging.

Software Foundations is great: https://softwarefoundations.cis.upenn.edu

If you stick with it long enough, you'll even build up to Hoare logic which is the underpinning the tools like dafny use to generate the equations they throw to the solver.

A very good resource for both verifying code and functional programming is Software Foundations (https://softwarefoundations.cis.upenn.edu).

One note though: Verus and the tool Software Foundations works with (Coq) take different approaches to proving things.

Verus attempts to prove properties automatically using something called an SMT solver, which is an automated system for solving constraints. Coq on the other hand, requires you to manually prove much more, offering a more limited set of automations for proving things.

Both have their advantages and disadvantages, namely that automation is great when it works and annoying when it doesn't.

(Another side note: Zero Knowledge Proofs (ZKPs) are kind of something different. A great many people who work in formal verification/proof don't touch ZKPs at all (ex: me). They are better thought about as a cryptography primitive)

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.

Enforcing the type hints at runtime gets really expensive if you allow for complex/higher order types. Typed Racket has had trouble with this since it tries to actually be a sound gradual typing system. Interesting work here: https://dl.acm.org/doi/pdf/10.1145/3434334 on speeding it up via static analysis (figuring out what dynamic enforcement points you can statically eliminate).

In fact Chomsky is repeatedly on the record of believing there are computational limits to humans.

For natural numbers you can form that first one in terms of the second one. Natural number can be through of as an inductive construction.

Either:

- Zero

- 1+ (another natural number)

Can you give an example?

Seeing Data-Centric Introduction to Computing (https://dcic-world.org)

It's written by Shriram Krishnamurthi, who is a really interesting researcher who cares quite a lot about CS education.

Reading the site, what's the catch? What is the monetization system?

The video linked in the article has been set to private, anyone know of a public version? Or a brief summary of the contents?

Flagging my two favorite introductions to computing:

How To Design Programs: [https://htdp.org]

A Data-Centric Introduction to Computing: [https://dcic-world.org]

Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.

Right, but you'd still need to synchronize that with some concurrency primitives (like a mutex or semaphore) and that has the potential for bugs. Whereas on an immutable structure can't suffer from that problem, which can make concurrent programming easier to reason about.

Slightly more to that, since it provides a mechanism for integrating it with existing C programs (so called, Interface Types or I-Types for short).

Much easier. It doesn't change the runtime representation of types at all. It also supports a gradual typing-esque system for adding more precise types onto existing languages without changing the source code.

Yes it is an attempt at being a formal model of that language.

Ok well _I_ was just defining the term. I didn't write the project. You will note they provide benchmarks with data showing the efficiency gain. What's left (as a reader) is evaluate the quality of those benchmarks.

"Beta Optimial" != Fastest Execution strategy for all kinds of code. Just defining the term, not arguing about it's engineering application.

GHC is not beta optimal, due to some complications around what happens when a closures are created. (This is `HOW.md` claims)

Yup, was just trying to give an example that utilized primitives to make it easier.