ratmice

18 ms·

181.
by ratmice 7y ago
Another thing to consider is it isn't counting all the rust dependencies. You can get away with a lot less code in tree when things get pushed out into crates.
182.
by ratmice 7y ago
It's using web2c, and linking against a cleaned up version of the generated C sources for a combined c/rust binary. There is a further project which runs c2rust over the generated c sources, and is cleaning up the generated c sour
183.
by ratmice 7y ago
not sure it is about aligning goals, It seems more like maximizing collaboration in spite of diverging goals, and doing so without compromising upon them. If your goals, and their goals either conflict or do not intersect, either one or bot
184.
by ratmice 7y ago
I've been in both situations of missing the 12 month boat, and rushing to get something in before the boat leaves port, and it's terrible. that said I think 4 weeks is a real short release cycle. 3 months, so 4 releases a year --
185.
by ratmice 7y ago
Indeed, most of the book https://leanprover.github.io/logic_and_proof/ is entirely term mode proofs, with tactics largely absent.
186.
by ratmice 7y ago
A bit weird, the article refers to "traditional beverages of countries rather than what is most commonly drunk by the populace today", but then uses images compiled from modern consumption data. "consumption (in litres of pur
187.
by ratmice 7y ago
One thing that helps is doing a vegetable scramble with anything that needs to be used up in the morning, falling back to shelf-stable cereals otherwise...
188.
by ratmice 7y ago
Aha, I had noticed a peculiar construction project near John Day recently, which may have been the early stages a BDA's. Here is another article from around the same time-frame as the one you linked, slightly east. https://w
189.
by ratmice 7y ago
Between the two authors here (McKinsey and Tarski), they cite each other 7 times, with 14 citations, giving 50% outgoing self-citation, however this paper also received incoming citations contemporaneously... https://doi.org&#x2F
190.
by ratmice 7y ago
Yes, the problem is that X11's login/lock screen is secured by grabbing the keyboard and mouse, taking away input focus from the login screen in many cases will allow you to bypass it entirely.
191.
by ratmice 7y ago
To give a list of these PL-level separation mechanisms, and their languages, these are the kernels I know of that work in this fashion. Spin OS (Modula-3), Singularity (Sing#), Midori (M#), TockOS (safe rust). As far as I know TockOS is the
192.
by ratmice 7y ago
Your comparison to the second amendment is not just "on the same level", but entirely accurate. To this day the United States Munitions List, classifies cryptographic devices under Category XIII Materials and Miscellaneous Article
193.
by ratmice 7y ago
One instance of this phenomenon is Knuth's TeX program, written in a dialect of Pascal which Knuth calls Pascal-H, accepted by Charles Hedrick's compiler: I believe the sources for the compiler can be found here, https:/&#x2
194.
by ratmice 7y ago
For some reason i would be suprised if they check for unicode roman numerals, https://en.wikipedia.org/wiki/Numerals_in_Unicode#Roman_nume...
195.
by ratmice 7y ago
I think it does already perhaps, http://genodians.org/alex-ab/2019-03-06-disposal-browser-vm discusses IIUC a disposable firefox instance, running in genode, which is run in either virtual box, or seoul vmm. Similarly
196.
by ratmice 7y ago
Also see this: http://www.michaelbeeson.com/research/CheckEuclid/index.php It seems a dependently typed language might be overkill, "The proofs described in this paper only need a rather weak logic. There are
197.
by ratmice 7y ago
I guess a pet peeve of mine, the Di, in Dialectic refers specifically to two-valued logic, resolving to a truth or false. Which at least in the case of Jain philosophy, with 3 basic truth values true, false, and unassertable, so really thes
198.
by ratmice 8y ago
i'm not sure i understand, but perhaps https://en.wikipedia.org/wiki/Pancyclic_graph
199.
by ratmice 8y ago
One can do this sort of thing in Ur i believe, which uses system F-omega with row polymorphic types, http://www.impredicative.com/ur/
200.
by ratmice 8y ago
From the other side of the fence, another thing to look at would be the decidability of presburger, and skolem arithmetic, the following paper then goes over the extensions of these, which render the result undecidable. http://ci
201.
by ratmice 8y ago
There is an odd mishap, when you are dragging one of the circle handlers, and drag outside of the gridded area, then through the center of the circle. It flips into a corner
202.
by ratmice 8y ago
I believe the reason they gave from the previous article was the bank has a branch in new york.
203.
by ratmice 8y ago
NLTSS as well
204.
by ratmice 8y ago
IANAL, but I find 2. weird, my first thought was that it obfuscation would give the opposing litigant an argument for willfulness potentially increasing patent damages. i.e. it may reduce the total sum of patent damages across all potential
205.
by ratmice 8y ago
personally, I will generally just want to construct some artifact which has some property, e.g. the proof is a program to construct something. Where a classical proof doesn't give you this program, it merely states that such a propert
206.
by ratmice 8y ago
I believe there are a couple of different claims being made in the above, I went ahead and just made a gist with some proofs (in lean) that try and hit some of the points about usage of law of excluded middle, double negation translation yo
207.
by ratmice 8y ago
Interestingly, there is the NIST dictionary of algorithms and data structures, which has been around since 1998, and was updated as recently as last week. https://xlinux.nist.gov/dads/
208.
by ratmice 8y ago
I don't believe that they did, at least last I read x86 was not a verification target. http://sel4.systems/pipermail/devel/2017-June/001477.html
209.
by ratmice 8y ago
Even before MS, there was UW/spin os, on the language modula-3, in the mid-90s http://www-spin.cs.washington.edu/
210.
by ratmice 8y ago
I'm not entirely sure where or when it was introduced, the first mention of it I could find was May 1989 (pg 25) ftp://ftp.cs.princeton.edu/reports/1989/220.pdf

More ›