curryhoward

16 ms·

121.
Show HN: Netflix Party – Synchronize Netflix Video Playback(stephanboyer.com)
58 points by curryhoward 11y ago|30 comments
122.
by curryhoward 11y ago
There are a few "stateless" password managers worth considering: 1) http://www.supergenpass.com/ 2) https://www.stephanboyer.com/post/101/hashpass-a-simple-stat... (disclaimer: I wrote #
123.
by curryhoward 11y ago
There are a number of weird things about this article that make it hard to get through: > For now, let’s talk about the type we’re going to generate for a particular value in terms of a generating function, $$F(x)$$ where $$x$$ can vary
124.
by curryhoward 11y ago
You may know this, but for those who might not: Fermat's Last Theorem and Fermat's Little Theorem are two totally different theorems (both about number theory). Fermat's Little Theorem: For any integer a and prime p, a^p is c
125.
by curryhoward 11y ago
> Here is a horror story from the good old days when men were men and used DirectX 7. Ugh. > Personally, I hate CONST with a passion, so I like this trick. Ugh. > PhysicalObjects could take damage. The air strikes did enough damage
126.
by curryhoward 11y ago
Far less, IMO.
127.
by curryhoward 11y ago
> That means the attack surface for accessing someone's account is NP hard, but N is always equal to 4. FYI, the "N" in "NP hard" is not a number. It stands for nondeterministic. The mention of "NP hard&quot
128.
by curryhoward 11y ago
Correct. One way to think of it is that running the program produces a proof of the theorem. But since the program is guaranteed to terminate with a proof (since all functions are total in Coq), why run it at all? Type checking is sufficien
129.
by curryhoward 11y ago
> let's just assume they mean the same thing and move to more interesting discussions They don't mean the same thing, and that is a poisonous attitude to have. Parallelism is about performance. Concurrency is about synchronizat
130.
by curryhoward 11y ago
You're technically right (multi-core CPUs can do true parallelism), but you were downvoted probably because your point was obvious (to the people who downvoted you). A multi-core CPU is basically multiple CPUs. The details (multicores
131.
by curryhoward 11y ago
Type signatures can completely encode specifications in systems with dependent types. Of course no mainstream programming language supports dependent types, but it's worth pointing out that in principle a type can encode any property c
132.
by curryhoward 12y ago
Perhaps it's true that many programmers don't realize the fundamental connection between typechecking and theorem proving (i.e., that they are the same thing). But that wasn't meant to be the point. The point is that when mos
133.
by curryhoward 12y ago
When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This project seems equivalent to adding a runtime check at each call site to ensure the arguments and return
134.
by curryhoward 12y ago
> For large enough n, we can construct a Turing machine that attempts to prove a contradiction in our current most powerful axiomatic system (let's say ZFC). What is n in this construction?
135.
by curryhoward 12y ago
> All you have to do is demonstrate that TMs can be simulated in JavaScript, and that's fairly easy to do since TMs are so bare-bones. Actually I think this is fairly non-trivial. Sure you could make a "compiler" that comp
136.
by curryhoward 12y ago
Pretty terrible (but harmless) interview question. It reminds me of a pointless question I was asked once: name the 4 access modifiers in Java. That was the day I learned about "package-private".
137.
by curryhoward 12y ago
I think the consensus is to go with the "big blob of text" approach. You mentioned that postal workers are the only people qualified to parse addresses—let them do it. The validation done on your end shouldn't be much more th