Viewing profile — 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 evalu…

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…

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 …

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…

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 S…

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 righ…

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 optin…

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 …

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 …

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 numb…

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 C…

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 o…

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 …

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).