mbid

8 ms·

31.
by mbid 8y ago
Lost in Math by Sabine Hossenfelder, which was published just a few months ago. It deals with how foundational theoretical physics has been led astray by aesthetic ideals, i.e. "lost in Math", because of the lack of new empirica
32.
by mbid 8y ago
So you think the key for understanding constructive logic is to understand some peculiar syntax for a fragment of it. Ridiculous, but sadly quite typical among type theory cultists.
33.
by mbid 8y ago
> In my own field of machine learning, itself an academic descendant of Gauss’s pioneering work, [...]. Yes, and I'm a descendand of Julius Caesar, Confucius and Charlemagne. I won't tell you this when introducing myself tho
34.
by mbid 8y ago
> It’s a fundamental axciom of software security that you can’t trust source, so you must diagnose the binary. What if you trust the build tool chain and can reproduce the binary from source?
35.
by mbid 8y ago
I think the author tried to give an example of an incomplete theory. Euclid's geometry minus the parallel postulate is an instance of that as the two different models show.
36.
by mbid 8y ago
The hardware of every chromebook I know is enough to run a terminal emulator and a browser. You can install a gnu/linux distribution on most x86 based chromebooks. Gnu/linux is arguably better suited for "serious" develo
37.
by mbid 8y ago
Let me clarify---some version of typed lambda calculus. The document linked here doesn't seem to deal with the untyped lambda calculus and much less so with properties that are stable under change of representation of computable func
38.
by mbid 8y ago
> Your argument here amounts to: if it's not descriptive, it must be prescriptive. By this argument, the entirety of pure mathematics is prescriptive. Is the idea of a semiring a description of a particular natural object? But it m
39.
by mbid 8y ago
I certainly didn't mean to imply that the programming languages ignored by these reasearchers are any good, on the contrary. It's just that I find the way these researchers sell themselves questionable. They don't have a theo
40.
by mbid 8y ago
> It doesn't assert how they ought to be (theorists, like everyone else, may express their opinion but this is not what the theory studies). It is a study of formal systems; basically, it's formal logic under a different name:
41.
by mbid 8y ago
This looks like it's (going to be) about a theory of programming languages as based on some form of the lambda calculus. I think it doesn't get pointed out enough that this is not a descriptive science but more of a normative theo
42.
by mbid 8y ago
A security app written in PHP. Nice touch.
43.
by mbid 8y ago
There are plenty of bullshit jobs in the software industry. Many things designers and graphics developers do is goon-ish. Design is mostly an arms race. Employees of big companies create new design languages and at some point the rest has t
44.
by mbid 8y ago
To defend against what? That some guy at twitter who saw the logs can login and change somebody's status? Anyway, I guess you're right, I simplified. It is kind of a valid point, although if I was this paranoid then I would never
45.
by mbid 8y ago
Reminder that none of this would be necessary if nobody reused their passwords.
46.
by mbid 8y ago
From wikipedia: "A unary operation f, that is, a map from some set S into itself, is called idempotent if, for all x in S, f(f(x)) = f(x)."
47.
by mbid 8y ago
> arbitrarily nested lists "Cool" as it might be, please don't inflict it on others.
48.
by mbid 8y ago
YAME, Yet Another Markdown Editor.
49.
by mbid 9y ago
Maximum.
50.
by mbid 9y ago
"Here, read my ramblings about the "Run Less Software" philosophy on my blog that loads 10MB of data for what could be a plain html + basic css page, among which you'll find 800,000 characters of javascript code to execu
51.
by mbid 9y ago
Thank god the author told us which songs he was listening to. The story would've been incomprehensible otherwise.
52.
by mbid 9y ago
> Protecting people’s information is at the heart of everything we do Thanks for striking down the bad guys, Facebook, our ever vigilant guardian of personal information.
53.
by mbid 9y ago
Finally. This will be great for the environment and especially the climate.
54.
by mbid 9y ago
Could your language affect your ability to save? https://www.ted.com/talks/keith_chen_could_your_language_aff...
55.
by mbid 9y ago
Not all knowledge is logic or maths.
56.
by mbid 9y ago
There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093 I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see so
57.
by mbid 9y ago
>By design, the answer is no. Toposes are models of intuitionistic bounded ZF. However, in general dependent type theories, including observational type theory, don't have (and don't want!) the powerset axiom. Why wouldn&#x27
58.
by mbid 9y ago
Yes they do. Look at popular music around the world. It's all slight variations of American popular music. I don't think this is only because of the dominance of English, but the two phenomena are definitely symptoms of the same
59.
by mbid 9y ago
Do we really want billions of people who all talk the same, think the same, and have the same values? I don't see how that could possibly be a good thing. The world is already bleeding ridiculous amounts of accumulated knowledge and wi
60.
by mbid 9y ago
> > Universes in type theory correspond to inaccessible cardinals/Grothendieck universes in ZFC or object classifiers in elementary toposes, at least informally (I doubt there is published work here). There is quite a bit of p

More ›