reuben364

7 ms·

31.
by reuben364 3y ago
There is also the tool of taxation and fines, which while in turn are backed by a threat of violence are not the black and white which you allude to.
32.
by reuben364 3y ago
And then Google slowly built a monopoly on browser implementations. Interoperability isn't appealing to corporations when users don't have much of a choice on using your platform.
33.
by reuben364 3y ago
Curious what your thoughts are on the paradox of tolerence? Google and the person hosting a static blog on a server in their basement are not the same.
34.
by reuben364 3y ago
Your "adverserial" mathematician phrasing made me chuckle at the the thought of a future where you have cybersec jobs in automated journals to prevent shady academics from using kernel bugs to spam fake submissions.
35.
by reuben364 3y ago
Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).
36.
by reuben364 3y ago
One distinction in Nix vs Docker is that Nix has a dag structure as opposed to a singlely linked list structure of layers. The "writeText" function produces a derivation (basically an atomic build recipe) that produces that file.
37.
by reuben364 3y ago
I deeply regret the courses I barely passed. And the courses for which I had prior knowledge to pass comfortably but not engage on the nuances.
38.
by reuben364 3y ago
Surely the frequency of the vibration matters too? I would suspect that motorcycles will be closer to the resonant frequency of the springs. I don't pretend to understand enough to say with confidence though.
39.
by reuben364 3y ago
I had a friend that had a record linkage problem which interested me and so I dove down a rabbit-hole of Markov logic, but didn't see any mention of Naive Bayes approach when doing so. Although I don't really have any expertise in
40.
by reuben364 3y ago
An example from South Africa: https://en.wikipedia.org/wiki/Searching_for_Sugar_Man
41.
by reuben364 3y ago
Your description of neural rendering techniques reminds me of a video ( https://www.youtube.com/watch?v=6aXx6RA1IK4 ) where someone used a genetic algorithm to represent videos in Geometry Dash levels.
42.
by reuben364 3y ago
My CS degree (University of Cape Town) was basically a software engineering degree with a light sprinkling of theory. Basically our only proof that I remember was the the halting problem, and it was really only the basic idea with not much
43.
by reuben364 3y ago
Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Softw
44.
by reuben364 3y ago
At the worst of times, when I had a university assignment I would sit at my desk to do the assignment and physically feel a repulsive force from my work. Like a really strong gust of wind. And now I have unlocked middle school memories of s
45.
by reuben364 3y ago
With my ignorance of the python packaging ecosystem, I was always under the impression that requirements.txt was the version constraints, not the lock file.
46.
by reuben364 3y ago
Isn't dt, to delete up until and df, to include. I'm guess either you have config or it's so ingrained in muscle memory that there is a mismatch between what you type and what you think it is. When I played piano there was a
47.
by reuben364 3y ago
Whoops, forgot to eta expand.
48.
by reuben364 3y ago
Trying out the thing, and since this is ycombinator after all: type Lazy<A> = () => A; const lazy = <A,>(f: Lazy<A>) => { let thunk: Lazy<A> = () => { throw null; } thunk = () => { con
49.
by reuben364 3y ago
1. Haven't read too deeply, but aren't we working with FOL in this type system anyway (Well, Henkin semantics of HOL, I believe) 2. I guess the major semantic difference is that in one, you define a family of PERs for terms in a g
50.
by reuben364 3y ago
I wonder what the optimal encoding is given a list of banned words for any substring of a message.
51.
by reuben364 3y ago
ZFA (1908) had urelements. You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union. Even in type theory you have Church VS Curry style as to
52.
by reuben364 3y ago
Asking here because I can't find the the right google keywords. I see that m.reddit.com no longer works. Has it been that way for a while? EDIT: It's been redirecting to reddit.com since at least 2021
53.
by reuben364 3y ago
You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires
54.
by reuben364 3y ago
I saw rumblings about the AMA maybe beating the most downvoted "Pride and accomplishment" comment. Thinking of that I just yesterday got Diablo 4 and realized just how normalized always online, microtransactiony BS has become. May
55.
by reuben364 3y ago
Yes, but the point is that you are giving a constructive existence proof for that bound. You asked for why there are so few total languages. The answer, as far as I'm aware, is either brute force on a fixed amount of memory or giving p
56.
by reuben364 3y ago
I guess the alternative is just bounding the number of instructions and proving inside or outside your language that it is sufficient for your program.
57.
by reuben364 3y ago
BRB, implementing a x86 interpreter with O(2^n) memory overhead.
58.
by reuben364 3y ago
While Lean4 is meant to be much more of a general purpose language than it's predecessor, it is still built with being a proof assistant in mind. That being said it is self hosted and has been in development and use for quite some time
59.
by reuben364 3y ago
Perhaps a more generous interpretation is that just because a self-driving performs better than humans overall doesn't mean it performs better the specific situations you drive in. Though even then I think it might be dubious.
60.
by reuben364 3y ago
Ah, you don't need linear types for that. Linear types will prevent you from duplicating or discarding values, but all you need is to only allow "final state" values to be used in your API. Also a reminder that I should read

More ›