Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
mietek
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
16 ms
·
151.
▲
by
mietek
8y ago
AlphaGo is a hybrid system, using deep reinforcement learning and Monte Carlo tree search. Tree search dates back to Shannon, before neural networks. AlphaGo is a triumph of symbolic as well as statistical AI.
152.
▲
by
mietek
8y ago
> There is no question of who the experts are: anyone can invest in a prediction market You mean: anyone that has the opportunity to invest. Incidentally, prediction markets have failed to predict the outcomes of the 2016 US presidenti
153.
▲
by
mietek
8y ago
The answer should be clear at this point. WhatsApp provided too much privacy and not enough monetisation opportunities.
154.
▲
by
mietek
8y ago
Standards have been lowered. Here’s a perspective from someone who used to be a tenured lecturer in the UK: http://www.marktarver.com/professor.html
155.
▲
by
mietek
8y ago
> Not in the sense of worst-case time complexity. Fair enough.
156.
▲
by
mietek
8y ago
> Proving equivalence between programs is not computable (by easy reduction to the halting problem), and infeasibly expensive to do manually for non-trivial programs. Barring unexpected breakthroughs in algorithms (e.g. a constructive p
157.
▲
by
mietek
8y ago
Here’s one from my student days: We define the derivative of a party as the amount of alcohol that can be purchased by returning the empty bottles left after the party. A good party is a party such that the second derivative of the par
158.
▲
by
mietek
8y ago
Reformatted, with inline figures and corrected references: https://github.com/mietek/pol
159.
▲
by
mietek
8y ago
Indeed, the objection is against the method by which this system is supposed to be defined. As you say, we start with an implicit assumption that we don’t have an effective procedure to construct the set of statements that are true in th
160.
▲
by
mietek
8y ago
You may be working in classical logic, but that doesn’t mean the parent poster is. You asserted the parent poster seems to be confused, but what the parent poster said makes sense in a constructive setting. Please see my other comment: h
161.
▲
by
mietek
8y ago
You seem to be forgetting that constructive truth means provability. Also, it doesn’t seem right to use the informal “take” when the object in question is not computable.
162.
▲
by
mietek
8y ago
You are invoking a classical notion of existence. This is not acceptable to a constructivist, for whom “a statement is true if we have a proof of it, and false if we can show that the assumption that there is a proof for the statement l
163.
▲
by
mietek
8y ago
Note HN has hellbanned your account, and your comments are showing up as dead.
164.
▲
Video tour of Macintosh factory in Fremont, CA (198?)
(youtube.com)
1 points
by
mietek
8y ago
|
0 comments
165.
▲
by
mietek
8y ago
This would have been a content-free article if not for the beautiful photos. Here’s a video tour of the Macintosh factory that used to be in Fremont, CA: https://www.youtube.com/watch?v=Dk306ZkNOuc
166.
▲
by
mietek
8y ago
Two sentence summary that glosses over a lot of things: 1. Types can be used to classify programs. 2. Dependent types can be used to classify programs by running other programs on them. If you would like to learn more about dependent types,
167.
▲
by
mietek
8y ago
> Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really understand … One sentence summary that glosses over a lot o
168.
▲
by
mietek
8y ago
The very first photo on the page (Chapter 1) shows a plugged-in power cable.
169.
▲
by
mietek
8y ago
I share your sentiments. With regards to Genera, have you seen this? https://static.loomcom.com/genera/genera-install.html
170.
▲
by
mietek
8y ago
> …the opaqueness was not conducive to creating a culture of power users and "semi-developers" unlike the PCs of the time. Utter nonsense, as anyone who has ever used ResEdit can tell. http://basalgangster.macgui.c
171.
▲
by
mietek
8y ago
Do any hard-core A/UX fans happen to have a copy of the A/UX Device Drivers Kit, or the Building A/UX Device Drivers manual?
172.
▲
by
mietek
8y ago
> It shows that no significantly expressive system can be designed that won't allow paradoxical statements. The above is a complete misrepresentation of Gödel’s second incompleteness theorem. The theorem holds for any sufficientl
173.
▲
by
mietek
8y ago
Inevitably, I’m going to have to ask for a reference.
174.
▲
by
mietek
8y ago
The Gibbs lecture can indeed be found in Kurt Gödel, Collected Works, Volume III, Unpublished essays and lectures, edited by Feferman et al., 1995. http://libgen.io/search.php?req=godel+collected+works+3&open...
175.
▲
by
mietek
8y ago
Could you give a reference for this claim of Wittgenstein’s, please?
176.
▲
by
mietek
8y ago
> … strong typing … C … This is incorrect. Wikipedia specifies C’s typing discipline as “static, weak, manifest, nominal”, which isn’t great, but is at least in the right ballpark. “Strong” and “weak” are unhelpfully overloaded words
177.
▲
by
mietek
8y ago
> that is why the Soviet Union lagged U.S. technology https://en.wikipedia.org/wiki/NK-33
178.
▲
by
mietek
8y ago
The specific experiment proposed by Deutsch is not yet possible to perform in practice.
179.
▲
by
mietek
8y ago
In his 1985 paper, “Quantum theory as a universal physical theory”, Deutsch writes: > I have pointed out several times in the preceding sections that the C.I. and the Everett “interpretations” are really different formalisms for quantum
180.
▲
by
mietek
9y ago
> Some inventions seem genuinely prescient, like a collection of animated proto-emoji stickers. Some are impractical but fascinating, like a “town” computing interface with buildings for apps. I wonder how many other have never heard o
More ›