ezyang

21 ms·

121.
by ezyang 14y ago
We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.
122.
Gamifying mathematics (an interactive tutorial for sequent calculus)(logitext.ezyang.scripts.mit.edu)
54 points by ezyang 14y ago|4 comments
123.
by ezyang 14y ago
But it really is mind-bending: if you, instead, add a theorem to the system (say, ZFC) which states, "ZFC is consistent", this system (ZFC+Con(ZFC)) is consistent! Even more strangely, if you instead add "ZFC is not consistent", this system
124.
by ezyang 14y ago
I think Simon Marlow's comment sums it up. "Welcome to Jon Harrop's magic world where everything is not as it seems!"
125.
by ezyang 14y ago
Suppose you have a system, but for legal liability reasons you cannot have this system be open to users (say it's a medical system, and having untrained people fuck around with it messes with certification.) However, you make it reasonably
126.
Use the source, don't read it (comic)(blog.ezyang.com)
2 points by ezyang 14y ago|0 comments
127.
by ezyang 15y ago
It's a replacement in the sense that, whenever you'd type 'ssh', you should type 'mosh' instead.
128.
by ezyang 15y ago
So, the thing that always gets Haskell folks when dealing with an implementation (2) is that you can't get uniform data representation when dealing with things like arrays. It means you have to unbox things. Arguably, the situation is not m
129.
by ezyang 15y ago
I know how to do precise GC if you allow me to add a (pointer-size) header to all data living in the heap; i.e. to maintain the RTTI. I don't know how you do that if you're not allowed a header. Do C# and D have headers?
130.
by ezyang 15y ago
Funnily enough, I understood why they went the conservative GC route. It has to do with the overall Go philosophy, which is that they really do not want features to affect data representation. This has meant no boxing (and no easy polymorph
131.
by ezyang 15y ago
I'm not the biggest fan of the solution in the article; but my biggest problem is that you're using floating points as keys for your hash table. Fix comparison for floating point? Well, now you're violating the IEEE standard. Introduce a ne
132.
by ezyang 15y ago
Did you run the code? The reason why the behavior here is bad is because Python uses probing to implement hash collision detection. Essentially, once you've looked up the hash, you have to check to make sure the value stored at this hash is
133.
by ezyang 15y ago
Which is distinct from a "totally random hash function", which is a hash function for which the hash associated with every value is uniformly randomly selected from the key space. Totally random hash functions have very good properties, but
134.
by ezyang 15y ago
As something of a glorified preprocessor, there is a limit to how much it can "make the language better". However, they will probably be able to get a bit of hacker mileage out of code generation, and I can see how you could add features wh
135.
Visualizing Range Trees(blog.ezyang.com)
3 points by ezyang 15y ago|0 comments
136.
by ezyang 15y ago
I've just done so, and I intend on keeping Web History turned off. I simply do not derive enough benefit from having this data around for myself (when's the last time you benefited from Web History), and unlike other permanent data such as
137.
by ezyang 15y ago
Confinement would certainly be one way of getting "theorems for free" about untrusted code. But it doesn't work for all types of things you might want to prove.
138.
How to build DRM you can trust(blog.ezyang.com)
7 points by ezyang 15y ago|2 comments
139.
by ezyang 15y ago
> The backdoor was not in the main code in SVN or in Git, which specifically protects against this exact problem Pedant alert, but Subversion doesn't protect against malicious manipulation; it doesn't checksum its commits.
140.
by ezyang 15y ago
Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using someth
141.
by ezyang 15y ago
I agree that at this point, it's completely unsuitable for the staples of college mathematics (e.g. calculus, differential equations), although it was not clear non-mathematicians were being subject to any sort of rigor anyway. That said, t
142.
by ezyang 15y ago
There are areas of mathematics for which proof assistants do a much better job; here is an interesting presentation using the theorem prover Coq as a virtual TA for discrete math: http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdf
143.
by ezyang 15y ago
I think this link is a much better treatment of the famous "Benny" experiment: http://blog.mathed.net/2011/07/rysk-erlwangers-bennys-concep... (with a bonus of less conflict-of-interest.)
144.
by ezyang 15y ago
Here is another way of defining something is sorted, taken straight from a real language: Inductive StronglySorted : list A -> Prop := | SSorted_nil : StronglySorted [] | SSorted_cons a l : StronglySorted l -> Forall (R
145.
by ezyang 15y ago
A large an interesting part of being a philosopher involves logic in its purest sense, but it wouldn't right to claim that this is all philosophy is.
146.
by ezyang 15y ago
MultiParameterTypeClasses are a fine feature! It's the ones like UndecidableInstances that you have to be careful about.
147.
by ezyang 15y ago
Note that this is not perfect; frequently, in order to use a module using some language features, you need to enable these language features yourself (the interface may be in-expressible without the language extensions!) But they don't seem
148.
by ezyang 15y ago
This is accurate. Ethan Zuckerman has more commentary on the topic here: http://www.ethanzuckerman.com/blog/2011/12/28/exploring-the-...
149.
by ezyang 15y ago
We understand the tuning parameters for these processes a bit more since this post was written a year and a half ago (We hit a magic phase shift for our other FastCGI processes, at which point our servers started falling over from 4000 user
150.
The upcoming war against general purpose computing (transcript)(github.com)
4 points by ezyang 15y ago|0 comments

More ›