ocfnash

44 ms·

31.
by ocfnash 5y ago
You lucky thing! My wife and I visited Réunion in 2019 and absolutely loved it. One thing that struck us was just how much it felt like what it is: a piece of France in the tropics. We had just come from Mauritius which felt quite remote bu
32.
by ocfnash 5y ago
I interpret this as a simple thinko, not unlike the expression "I could care less". As Al Yankovic says: 'Like "I could care less", That means you do care, At least a little'
33.
by ocfnash 6y ago
I think it's unlikely the lights happened to send the right IR pattern. I once hooked a TV remote up to a logic analyser to have a look and here's how the on/off signal looked for this brand: http://olivernash.org&
34.
by ocfnash 6y ago
The Lean Community website [1] is a great place to start. Depending on your background you might like to dive right into the Natural Number Game [2] or the Theorem Proving in Lean [3] (both linked from the Community site). 1. https:/&
35.
by ocfnash 6y ago
Threading the cores is indeed quite fiddly. I think back in the day, large numbers of seamstresses pivoted into manufacturing core memory!
36.
by ocfnash 6y ago
You can buy core memory kits [1] for adding core memory to an arduino. They only give 8x4 but you could get to "cordmp" with a five-bit encoding ;-) The vendor, with whom I have absolutely no affiliation except for exchanging a fe
37.
by ocfnash 6y ago
I also did pure mathematics, and this summarises my experiences perfectly.
38.
by ocfnash 6y ago
Rumour has it doing a PhD might actually be a rewarding experience in its own right, and not derive its value solely from the possibility of remaining in academia.
39.
by ocfnash 6y ago
Coq uses this notation for (propositional) and and or.
40.
by ocfnash 6y ago
Compiler bugs are indeed pretty frightening. A few years ago I bumped into one in some code that had potential to have a big impact. Unfortunately I am not at liberty to give details about the business setting except to say that we had proc
41.
Building geometry solvers for the IMO Grand Challenge(jesse-michael-han.github.io)
2 points by ocfnash 6y ago|0 comments
42.
by ocfnash 6y ago
Not strictly related but I recall once hearing that Bach may have never heard his Brandenburg concertos performed. Looking at Wikipedia now I see: "Because King Frederick William I of Prussia was not a significant patron of the arts, C
43.
by ocfnash 7y ago
I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types. I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit
44.
by ocfnash 7y ago
I love this write up, and while the solutions discussed are excellent, I think the general-purpose FM Index data structure might work even better. I confess I'd have to read this post more closely to be sure, but I find the FM Index da
45.
by ocfnash 7y ago
Great job; we need more good citizens like you! I was unaware that they do at least have the implied 620 figure for the entire US correct, so there is hope that this is just a localised typo. I can't get over how stunningly-similar thi
46.
by ocfnash 7y ago
Just a moment, 0.72% x 0.03% = 0.0002%, which is about 2 out every 1,000,000.
47.
by ocfnash 7y ago
"The crew went around, climbed to 8500 feet, depressurized the aircraft, opened the cockpit side window and cleaned the windscreen by hand."
48.
by ocfnash 7y ago
I did not miss this statement; for me this does not constitute a recommendation. Indeed I think many of the researchers of whom she is critical could claim that this is what they're doing.
49.
by ocfnash 7y ago
I dare say the author is right on many points but statements like: "But for all I can tell at this moment in history I am the only physicist who has at least come up with an idea for what to do." make it hard for me to share her p
50.
The Unison language(unisonweb.org)
262 points by ocfnash 7y ago|141 comments
51.
by ocfnash 7y ago
Note that finite-time singularities for the good old Newtonian n-body problem have been known to exist for quite a while. (See for example [1].) It's curious to think that a mathematical phenomenon like this can hint at new physics. [1
52.
Rigorous Mathematics(xenaproject.wordpress.com)
3 points by ocfnash 7y ago|0 comments
53.
by ocfnash 7y ago
I find this amusingly reminiscent of the Chinese Room: https://en.wikipedia.org/wiki/Chinese_room
54.
by ocfnash 7y ago
See also Verizon Math [1] for a different failure mode of utility company surcharge billing! [1] https://www.youtube.com/watch?v=MShv_74FNWU
55.
by ocfnash 7y ago
If anyone even uses it at all! I have a friend who works in a sales role for IBM. He told me that part of his bonus is contingent on being able to prove that the customer has actually installed the software which they bought. The policy app
56.
by ocfnash 7y ago
> After reading this, are you really any wiser now on the topic of quotients in Lean? Only a little but I'm hoping that some weekend reading up on Canonicity and Subject Reduction (now that I know these are the issues at play) will
57.
by ocfnash 7y ago
I strongly recommend reading https://github.com/coq/coq/issues/10871#issuecomment-5404526... which was written a few hours ago broadly in the vein of Lean vs. Coq, more precisely on the issue of how Lean hand
58.
by ocfnash 7y ago
According to Chekhov: "One is shy of asking men under sentence what they have been sentenced for; and in the same way it is awkward to ask very rich people what they want so much money for, why they make such a poor use of their wealth
59.
Stein's Paradox: better than average estimation [pdf](statweb.stanford.edu)
2 points by ocfnash 7y ago|0 comments
60.
Fractalize That(bit-player.org)
3 points by ocfnash 7y ago|0 comments

More ›