GregarianChild

13 ms·

91.
by GregarianChild 6y ago
This 'baggage' are statements like sqrt(17) ∈ log(.) (where (log(.) is the logarithm function) which are syntactically valid and have a truth value, which depends on the exact nature of how you code up various mathematical
92.
by GregarianChild 6y ago
The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type
93.
by GregarianChild 6y ago
The MathInspector is nice. Reminds me of the "Incredible Proof Machine" [1] which I find to be a neat tool in teaching logic. [1] https://incredible.pm/
94.
by GregarianChild 6y ago
Regarding your question, I think mathematics and programming about the same: being precise ! Programming is much more demanding, much more unforgiving in this regard, because you are talking to a stupid machine, rather than a smart human.
95.
by GregarianChild 6y ago
None of Zuse, Babbage, Torres y Quevedo, Ludgate, Dickinson, Desch, Atanasoff–Berry, Mauchly / Eckert, nor many of the other pioneers of computing came via Hilbert and FOM problems. An important source of early computing was the pr
96.
by GregarianChild 6y ago
The generalisation of Curry-Howard to parallelism was outlined in early interpretations of linear logic, I think Abramsky's [1] was the first, there has been a lot more work in this direction since. A good place to start to understand
97.
by GregarianChild 6y ago
I think you need HKTs, in other words System F-omega , to carry out Rossberg's idea.
98.
by GregarianChild 6y ago
Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads
99.
by GregarianChild 6y ago
Another recent primer on in-memory / near-memory computing in [1]. Upmem [2] is also selling memory with on-board compute. A space that is slowly hotting up! [1] O. Mutlu, S. Ghose, J. Gomez-Luna, R. Ausavarungnirun, A Modern Primer
100.
by GregarianChild 6y ago
Thanks. I was not aware of this, since I've not worked on a Microsoft stack for a long time. Are those F# AOT compilers mature and support all features, including libraries? In this case F# would be a viable alternative to OCaml for Ja
101.
by GregarianChild 6y ago
I agree from a technical POV, but there is a social reason (network effect): Swift has Apple-backing, OCaml is not currently supported by any of the big, influential software companies. OCaml's main backer now is Jane Street who do a
102.
by GregarianChild 6y ago
gradient descent is faster and more efficient. Why? Regarding neuro-evolution and hyperparameter, here the question becomes why would the stochastic nature of GAs (and ESs) be particularly better than e.g. brute force search?
103.
by GregarianChild 6y ago
An interesting question is: why are we not seeing fast and scalable GPU implementations of GAs? (I'm not trying to trick you, genuinely curious). I think one problem, making GAs as they are understood today (maybe
104.
by GregarianChild 6y ago
The problem you describe (model architecture will work for which problem) is not lacking rigour, but due to the Turing complete expressive power of neural networks. What you can do is use the existing rigour and derive stronger properties
105.
by GregarianChild 6y ago
That's not because of lacking rigour, but because of complexity! You cannot, in general, predict arbitrary program properties without running programs, that's the essence of Rice's theorem [1]. By the famous Universal Appro
106.
by GregarianChild 6y ago
In what sense are neural nets not rigorous? The whole pipeline from Pytorch or TensorFlow and Python to LLVM, to GPUs or TPUs is absolutely rigorous. Much more rigorous, in fact, than normal, hand-written mathematics, as you find it in
107.
by GregarianChild 6y ago
Taiwan never had a lockdown! See the discussion here: https://news.ycombinator.com/item?id=25539398 Taiwanese policies were not just much more successful in containing the virus, but also much less draconian.
108.
by GregarianChild 6y ago
The paper you cite is from 2014 and the mitigations discussed there have all been circumvented. [1] is from 2020 and a better read for Rowhammer mitigation. [1] J. S. Kim et al, Revisiting RowHammer: An Experimental Analysis of Modern DRAM
109.
by GregarianChild 6y ago
Isn't ChipKill just another form of ECC? If so there is a number of bitflips that ChipKill can no longer correct / detect. [1] seems to say that they observed some flips in dRAM with ChipKill, although the paper is a bit vague her
110.
by GregarianChild 6y ago
One might wonder if the EU has leadership capacity to be able to maintain domestic strategically important industries. Generalising from 40 years of EU history, I have little confidence. The top US and East Asian processor and semiconducto
111.
by GregarianChild 6y ago
aerospace, energy, semiconductors, telecom, drugs/biotech The EU lost leadership in all of them! (And some others!)
112.
by GregarianChild 6y ago
The RISC-V foundation moved to Switzerland primarily to help the big Chinese processor companies to work on RISC-V. Regarding the EU heavily betting on RISC-V , what gives you confidence that this will work? The history of EU funded projec
113.
by GregarianChild 6y ago
HiSilicon / Huawei is yet another player making CPUs and GPUs. Pretty big, too. Although having lost access to TSCM in 2020 is going to hit them hard.
114.
by GregarianChild 6y ago
From the article: Hedge fund Third Point, who are said to own > $1B of Intel shares, is pushing Intel to explore whether it should keep chip design and production under one roof. This is in response to Intel's having lost to TSMC a
115.
Hedge fund urges Intel to explore deal options(reuters.com)
2 points by GregarianChild 6y ago|1 comments
116.
by GregarianChild 6y ago
The UK is no island?
117.
by GregarianChild 6y ago
What do you find objectionable about Taiwan's Covid response, taking into account its success, not to mention the cost (in a general sense) of quarantining whole countries (which means restricting the freedom of millions of health citi
118.
by GregarianChild 6y ago
Could you elaborate by which moral principle you come to the conclusion that a vague slippery slope and even more vague outrage is more important than stopping a pandemic with hundreds of thousands of preventable deaths? Most moral sys
119.
by GregarianChild 6y ago
Copy Taiwan. No country has been dealing better with Covid than Taiwan. No lockdown, and > 200 days without new Covid case [1]. Taipei had daily direct flights from Wuhan, and the Diamond Princess mooring near Taipei. They told the wo
120.
by GregarianChild 6y ago
Why do and then un-do? The reason is that we've not yet found a better way of making fast general purpose processors. The OOO (= out-of-order) approach with high-quality prediction (e.g. branch, value) to processor micro-arc

More ›