ratmice

9 ms·

91.
by ratmice 3y ago
Not all lean proofs are actually computable, see the computable function link in the url you gave.
92.
by ratmice 3y ago
Instead of using labels (e.g. to avoid unused_label) and because labels are most commonly used as the target of a goto. gdb also supports `break -probe foo:bar` when placing some `DTRACE_PROBE(foo, bar)` at the appropriate line. I think th
93.
by ratmice 3y ago
Another cool museum, https://theoremprover-museum.github.io/
94.
by ratmice 3y ago
Apologies, too late to edit
95.
by ratmice 3y ago
> This is a lead-in to a longer term vision of introducing a “pinned effect.” Seems really weird, pinning is not an effect, if anything it suppresses an effect (move). Edit: I guess i should have kept reading the next paragraph, where he
96.
by ratmice 3y ago
There is a park in my neighborhood, half of which is designated as a nature play space. Where all those things are allowed, lots of forts. It appears it was associated with the national wildlife federation natural learning initiative. htt
97.
by ratmice 3y ago
If you look at https://ocapn.org/ (linked within the original submission, The group is comprised of: * Agoric * The Spritely Institute * Cap'n Proto * Many other independent experts and interested parties from Cap&#x27
98.
by ratmice 3y ago
Yeah, I think the catch is the "pre-existing property specifications" part. I think you need to carefully understand both AI & Human generated propositions. While proofs once checked are just gravy.
99.
by ratmice 3y ago
> Debugging complex code is hard, first simplify, then debug I've always made it a point to do a first pass just reading code and forming a hypothesis about the problem (which is often wildly wrong) before making any changes or even
100.
by ratmice 3y ago
I did an experiment with my cat for about a year, trying to ascertain preference with about 5 baskets filled with blankets. Blankets would be swapped and baskets moved around daily. It had an obvious favorite blanket previously ascertained.
101.
by ratmice 3y ago
Don't you mean something like [A+B+C] ≃ [A]×[B]×[C]
102.
by ratmice 3y ago
Yeah, excessive modularity can be just as bad as any monolith. I'd tend towards sticking to a few libraries with well defined boundaries like target OS, or perhaps one for native cpu architecture word sizes and the like. But that stil
103.
by ratmice 3y ago
While it is true that things don't move fast, there have been proposals to it which have seen some adoption (thinking MONO_BUFFER was implemented by smlnj has compat in mlton). And I recall a proposal from polyml subsequently was impl
104.
by ratmice 3y ago
It is used in The definition of Standard ML to define the syntax and semantics of the language. That is the most "in the wild" usage I'm familiar with in the sense that it gives a formal specification of the language, which
105.
by ratmice 3y ago
Also in that same screenshot, hurd used to drop you into a shell as the nobody user where you could run the login binary... Curious if that was changed as part of debian, or changed for some other reason.
106.
by ratmice 3y ago
It is easier to just use `XGetIconSizes` on the `DefaultRootWindow` than try to pull it out of configs or doing some kind of plist parsing. Here is the function GNUstep uses... It should not be difficult to pull the relevant stuff out for
107.
by ratmice 3y ago
I don't develop for GNUstep anymore, but I remember making scalable dock apps possible some decades ago. You need to configure the size of icon windows in windowmaker WPrefs, the app then needs then to query the [[[NSApp iconWindow] c
108.
by ratmice 3y ago
Of course, rust being nominally typed it is a distinct thing, while TS is structural. But that aspect should affect much more than just unions, (that said I personally know very little about typescript so talk my opinions here with a grain
109.
by ratmice 3y ago
Rust actually does have an untagged union type, but it generally requires some unsafe to use it, doesn't seem to get much use beyond c/ffi.
110.
by ratmice 3y ago
I've read a similar thing about pink dogwood, where growing a seedling from it will only have a small chance of being another pink dogwood, more likely than not producing a white one. Because of that they are typically cloned.
111.
by ratmice 3y ago
The impetus for python, rather than making a call into the inferior/debugged process is largely to support pretty printing data structures within core files & crash dumps. While it is certainly possible, it is not a small amount o
112.
by ratmice 3y ago
It probably can't be understated though how important it was that Ton, the original author was spearheading that whole thing. He would have had both an existing relationship with the investors, and enough clout with the community backe
113.
by ratmice 3y ago
I have Also heard of https://www.14trees.com/ and terran robotics doing this... Edit: I imagine though, that in locations where building is regulated under the international residential code. There has been less investment
114.
by ratmice 3y ago
As a counterpoint, restricting the scope of the CoC to the confines of the project allows people to harass others directly, via DM's, email, etc with impunity. I am at least relieved by may in "violations of this code outside t
115.
by ratmice 3y ago
I guess though I'm kind of curious why they don't just raise their rates to the account for the actual cost of insuring there? I assume probably some regulation or volatility...
116.
by ratmice 3y ago
The only thing I know of that provides a desktop is genode, which can run on top of seL4 (but also quite a few other kernels). Given that it'll be more like dinking around with genode than seL4 proper, exactly because of this multi ker
117.
by ratmice 3y ago
Interesting I've always been allured by the prospect of parser generators for unified parser/lexers like ebnf & regular right part grammars, so it is nice to hear some of the downsides of these approaches that had never really
118.
by ratmice 3y ago
Matt Might also did an article about lexing with regex derivatives. https://matt.might.net/articles/nonblocking-lexing-toolkit-b...
119.
by ratmice 3y ago
Seems obvious to me that ease of installation seems also is a factor where popularity can have an impact. If one is more popular that increases the likely hood that users will already be familiar with installation methods (ignoring actual
120.
by ratmice 4y ago
One thing which perhaps is not captured well in the article, is that rather unlike when reading/writing source code, where stepping through lines of code is a relatively uncommon task only done debugging. For interactive theorem prove

More ›