opnitro · HackerTrans

opnitro

no profile record

投稿

Breaking Free from Neural Networks and Dynamical Systems (2021)

lifeiscomputation.com

5 ポイント投稿者 opnitro2 年前0 コメント

Democracy at Work, Talks at Google (2017)

youtu.be

1 ポイント投稿者 opnitro7 年前0 コメント

What Is Democracy [video]

youtu.be

1 ポイント投稿者 opnitro7 年前0 コメント

Idris 2: Type Driven Development of Idris

youtube.com

4 ポイント投稿者 opnitro8 年前0 コメント

Long Live Shadow Socks

github.com

1 ポイント投稿者 opnitro11 年前0 コメント

コメント

2 年前議論

Do you have a link?

2 年前議論

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.

2 年前議論

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

2 年前議論

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.

2 年前議論

Lot's of great work on dafny in general!

2 年前議論

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.

2 年前議論

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)

2 年前議論

ya got me

2 年前議論

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)

2 年前議論

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.

2 年前議論

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!

2 年前議論

I'm guessing it's a reference to Go

2 年前議論

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.

3 年前議論

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

3 年前議論

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

3 年前議論

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)

3 年前議論

Can you give an example?

4 年前議論

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.

4 年前議論

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

4 年前議論

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