ratmice

7 ms·

61.
by ratmice 2y ago
I think the article is referencing two different cases, and the ones invalidated don't seem related to oximetry, I'm not sure what happened with the oximetry one though.
62.
by ratmice 2y ago
I'm not much of an openbsd user, but I have been meaning to understand if this is the hole execpromises is intended to fill. At the very least, I think execpromises was added a year after the documentation that you linked, so it's
63.
by ratmice 2y ago
Yeah, I don't know why we would need a limit, I'm sure if a temper tantrum devolves into one of them building their own robo army. The others will follow suit and it will all just balance itself out.
64.
by ratmice 2y ago
I know there is definitely some wonkyness with rust traits and type inference, // Uncomment for compiler error. // use serde_json as _; // // Because serde_json includes impl Partial
65.
by ratmice 2y ago
I think this qualifies as art. char insert_string1[]={"\n\r;\n\r"}; char insert_string2[]={";For some reason, inserting these lines makes it assemble correctly\n\r"};
66.
by ratmice 2y ago
John Francis in the comments seems to have (correctly) uncovered the mystery, looking at the homepage given in that comment via wayback machine has a link github with commits as recent as november.
67.
by ratmice 2y ago
I am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize.
68.
by ratmice 2y ago
Opinion, but lean and coq both use dependant type theory, while isabelle uses a first order logic. Between coq and lean, lean has always had great support for unicode, where coq always seemed to me ascii first, and coq itself predates the p
69.
by ratmice 2y ago
This is great, I can't wait to be able to use a NonMax type in place of NonZero in a couple of places.
70.
by ratmice 2y ago
Not the same a 3+4 but there are lemon roasted peanuts, I've not had them, but lemon roasted pistachio's are really good.
71.
by ratmice 2y ago
I don't think that the ghuloum 2006 paper was the initial basis for nanopass, at least the paper A Nanopass Framework for Compiler Education∗ seems to predate it in 2004 https://dl.acm.org/doi/10.1145/1016848.
72.
by ratmice 2y ago
Yeah, I never understood why they couldn't make it Dec-Feb-Jan with January at the end of the year so that Janus could still be the god of transitions, but I guess I'm no theologian so there is probably a reason.
73.
by ratmice 2y ago
My favorite technical debt is the off-by-two naming of quintilis through december from when they added Jan and Feb to the beginning of the calendar...
74.
by ratmice 2y ago
Alphabetical order is normal. http://www.ams.org/learning-careers/leaders/CultureStatement...
75.
by ratmice 2y ago
I would think the MISRA rules against dynamic memory allocation would present serious difficulty if not fundamental incompatibility when trying to implement web standards.
76.
by ratmice 2y ago
FWIW, as a long time user of tectonic I just started a project using typst yesterday, I'm really curious if typst will be able to do parallel downloading of packages than tectonic. This is something which I have found can affect initia
77.
by ratmice 2y ago
It is also about how easy rust makes it to use libraries, and depend upon external libraries as a part of your public API. C in particular makes this pretty inconvenient, so a lot of projects include data structures and things that other
78.
by ratmice 2y ago
It would probably be easier to enumerate the small number of projects which have a larger amount of maintainers. I think the vast majority only have a few maintainers.
79.
by ratmice 2y ago
There is also the notion that we have evolved a empathy for humans over other animals because it is beneficial. So that the 99.9% don't hunt down the .1% for sport.
80.
by ratmice 2y ago
In theory at least that precondition could be guaranteed by a newtype like SortedList without requiring any linear scan, that would work at least for most cases where lists are sorted by an algorithm. Though not necessarily custom data whic
81.
by ratmice 2y ago
I'm pretty torn, on the one hand this tight vscode integration should exist, and is being used to good effect by projects like the lean info-view, which shows the goals of the proof state. And my own project which e.g. generates railro
82.
by ratmice 2y ago
It honestly depends on how much your LSP server infests the editor. In the language server I wrote there are really 2 cases where we utilize the creation of an editor-specific extension * dynamic registration of file extensions * display of
83.
by ratmice 2y ago
I agree with the other commenter that his is not even remotely true... given something like loop { if (A) { ... } if (B) { ... } } 100% branch coverage means you've encountered both cases, but the loop could have encountered these
84.
by ratmice 2y ago
To me at least, the most difficult part of verifying rust code has been the lack of any pre/post conditions on the standard library, I quite often have ended up rewriting chunks of the std library, pulling them directly into my program
85.
by ratmice 2y ago
Yeah, `NonZero*` but also a type like `#[repr(u8)] enum Foo{ X }`, according to `assert_eq!(std::mem::size_of::<Option<Foo>(), std::mem::size_of::<Foo>())` you need an enum which fully saturates the repr, e.g. `#[repr(u8)]Bar
86.
by ratmice 2y ago
DCE has been around at least since 1971 Frances E. Allen's "A catalogue of optimizing trasformations", but I don't have her earlier papers/internal ibm memos to be able to say, but the section on DCE in that paper d
87.
by ratmice 3y ago
Regarding your almost query. There was a debate over Ogham space mark in unicode. It is considered whitespace though, with the rationale that it is sometimes visible, but sometimes invisible. Depending upon whether the text has a stem-line
88.
by ratmice 3y ago
ubergraphs are pretty weird, i've never actually seen them really used anywhere. Just a couple of papers pointing out their existence. They have some weird quirks like every hypergraph and thus graph has a dual, but ubergraphs with ube
89.
by ratmice 3y ago
XGrabKey?
90.
by ratmice 3y ago
What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there exists a function g inverse to f, and show something about the results of callin

More ›