cmrx64

28 ms·

331.
by cmrx64 9y ago
My favorite thing is when I search for a program, it comes up, I go to click on it or press enter, and then the web search finally comes back with the results and now I'm opening some browser with a random fucking web search. ARGH.
332.
by cmrx64 9y ago
Fair enough :) FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and
333.
by cmrx64 9y ago
In what way is HOL bizarre?
334.
by cmrx64 9y ago
Validation vs verification. Validation: "is this the right spec", verification: "does this meet the spec". Turns out once you have a formal specification, you can do all sorts of things with it that you couldn't do
335.
by cmrx64 9y ago
it's owner-programmable, which is a plus.
336.
by cmrx64 9y ago
plenty. not as many open source ones though.
337.
by cmrx64 9y ago
>Overcast is already so complex it can barely play a podcast without crashing if interrupted do you have a repro? I use overcast extremely heavily and haven't had a crash in a few months.
338.
by cmrx64 9y ago
Compares very favorably IMO, but you'll probably want to read their marketing pages or try it yourself.
339.
by cmrx64 9y ago
For years and years, packages shipped via FedEx would arrive at the house I grew up in beat to hell. Rarely to the point of damaging the goods inside, but not exactly confidence inspiring.
340.
by cmrx64 9y ago
yes. https://www.nist.gov/sites/default/files/documents/2016/10/1... https://www.cosic.esat.kuleuven.be/ecrypt/courses/albena11/s...
341.
by cmrx64 9y ago
I dunno. The stats are really super useful for insight into how REAL PEOPLE (not self-selected do-gooders) use the software, and also how new things (like Stylo!) interact with the many unique hardware, driver, software environments people
342.
by cmrx64 9y ago
1ML just shows that advanced (first-class) ML modules are really just System F_omega. That's just barely more than Haskell! More languages need to expose it nicely. But we already have most if not all the technology we need to make th
343.
by cmrx64 9y ago
http://llvm.org/pubs/ Ctrl+F for "data structure". It's actually the reason LLVM exists at all: http://llvm.org/pubs/2002-06-AutomaticPoolAllocation.html http://llvm.org&
344.
by cmrx64 9y ago
they are user-contributed.
345.
by cmrx64 9y ago
Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
346.
by cmrx64 9y ago
Yeah, external monitors in a mixed DPI setting is very weird. If you change your primary monitor, you get to pick which screen it looks OK on! Mine actually bricked itself so hard it couldn't boot at all. I had to send it back to dell.
347.
by cmrx64 9y ago
meanwhile, game and graphics developers are dying due to lack of modern opengl or, god forbid, opencl or vulkan.
348.
by cmrx64 9y ago
That's a reasonable concern. If Leo got hit by a bus the code quality would certainly suffer. He's pretty good about cleaning up PRs etc after merge, by which I mean, even if he isn't the only developer right now he does a lo
349.
by cmrx64 9y ago
No, it's not true, it "extracts" (compiles) to C++. < https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the
350.
by cmrx64 9y ago
> Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability. Not only is this unfounded, it's unreasonable. I can interpret "reliabilit
351.
by cmrx64 9y ago
Ahhhh I was wondering why my desktop suddenly started opening links in Edge!
352.
by cmrx64 9y ago
1. Denser (ie, more information per unit area) 2. More redundant (ie, more surface area can be destroyed and still be able to recover the original message)
353.
by cmrx64 9y ago
Because XUL will soon be unmaintained. It's too useful a tool to wither away and die.
354.
by cmrx64 9y ago
I have a story that is too long here about my struggles with math in high school, and while I'm maybe not the model CS student for a variety of related reasons, I think that I turned out mostly fine... None of the symbolic manipulation
355.
by cmrx64 9y ago
I've been an occasional user of Pencil for 5 years (almost to the month). Really glad to see it moving away from XUL.
356.
by cmrx64 9y ago
https://www.apple.com/apple-pencil/ https://en.wikipedia.org/wiki/Pencil Kind of already an established name in the English-speaking world. Serious talk though, this kind of comment is worthless.
357.
by cmrx64 9y ago
That particular benchmark stresses DOM and layout performance, that test just programatically clicks all the delete buttons in the page under test.
358.
by cmrx64 9y ago
It's poorly written overall.
359.
by cmrx64 9y ago
TFA looked at the copper concentration in the water after storage and it was below WHO guidelines for safe copper levels. Whether the WHO guidelines are sufficient or not is another question.
360.
by cmrx64 9y ago
This is usually called "fault injection". Check out https://blitiri.com.ar/p/libfiu/

More ›