opnitro

5 ms·

1.
Breaking Free from Neural Networks and Dynamical Systems (2021)(lifeiscomputation.com)
5 points by opnitro 2y ago|0 comments
2.
by opnitro 2y ago
Do you have a link?
3.
by opnitro 2y ago
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 shou
4.
by opnitro 2y ago
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
5.
by opnitro 2y ago
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
6.
by opnitro 2y ago
Lot's of great work on dafny in general!
7.
by opnitro 2y ago
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
8.
by opnitro 2y ago
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 differen
9.
by opnitro 3y ago
ya got me
10.
by opnitro 3y ago
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)
11.
by opnitro 3y ago
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
12.
by opnitro 3y ago
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
13.
by opnitro 3y ago
I'm guessing it's a reference to Go
14.
by opnitro 3y ago
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 tha
15.
by opnitro 3y ago
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:&#
16.
by opnitro 4y ago
In fact Chomsky is repeatedly on the record of believing there are computational limits to humans.
17.
by opnitro 4y ago
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)
18.
by opnitro 4y ago
Can you give an example?
19.
by opnitro 4y ago
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.
20.
by opnitro 4y ago
Reading the site, what's the catch? What is the monetization system?
21.
by opnitro 4y ago
The video linked in the article has been set to private, anyone know of a public version? Or a brief summary of the contents?
22.
by opnitro 4y ago
Flagging my two favorite introductions to computing: How To Design Programs: [ https://htdp.org ] A Data-Centric Introduction to Computing: [ https://dcic-world.org ]
23.
by opnitro 4y ago
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 la
24.
by opnitro 4y ago
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 con
25.
by opnitro 5y ago
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).
26.
by opnitro 5y ago
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.
27.
by opnitro 5y ago
Yes it is an attempt at being a formal model of that language.
28.
by opnitro 5y ago
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.
29.
by opnitro 5y ago
"Beta Optimial" != Fastest Execution strategy for all kinds of code. Just defining the term, not arguing about it's engineering application.
30.
by opnitro 5y ago
GHC is not beta optimal, due to some complications around what happens when a closures are created. (This is `HOW.md` claims)

More ›