It is fine though if people who don't knit enjoy knitting podcasts, but this is not that. Somewhere between the producer/consumer relationship there should exist some actual knitting. Otherwise (in cases like this) it's…
I'd also say a few things, if knitting takes a long time consider how long it takes to make a good clear pattern so that others can replicate it. People who make patterns are already dealing with a saturated market.…
Seriously? You can't get the feeling of satisfaction of wearing something, or having someone wear something you made from AliExpress. My point is your sense of feeling and validation is extremely distorted if you have…
Can't wear feelings and validation...
My only complaint with the article is that it doesn't seem to mention that digitized proofs can contain gaps but that those gaps must be explicit like in lean the `sorry` function, or axioms.
In FCC DA 26-68 they gave public notice of their change of interpretation/enforcement of the equal time rules to apply to this situation.
Maybe it can be done, but I struggle to believe adding in that branch for every forall quantifier (which may be plentiful in a proof) is going to help make a proof more understandable. Rather I feel like it'll just…
Rhetorical sentence? My point is that back-translation into natural langauge is translating into a less precise form. How is that going to help? No number of additional abstraction layers are going to solve human…
why do we invent these formal languages except to be more semantically precise than natural language? What does one gain besides familiarity by translation back into a more ambiguous language? Mis-defining concepts can…
> Proprietary use, commercial redistribution, or publishing modified versions with ads or tracking is strictly prohibited under GPLv3 or later. These all sound to me like "Further restrictions" which the GPL says: > If…
I feel like another optimization that rust code can exploit is uninhabited types. When combined with generics and sum types these can lead to entire branches being unreachable at the type level. Like Option<!> or…
I always feel that when saying lex/yacc style tools, it comes with a lot of preconceived notions that using the tools involves a slow development cycle with code gen + compilation steps. What drew me to the grmtools…
I would also say there is a 3rd class, which are distributed capabilities. When you look at a mobile program such as the GadgetBridge which is synchronizing data between a mobile device and a watch, and number of…
I couldn't agree with you more, the thing is our underlying security models are protecting systems from their users, but do nothing for protecting user data from the programs they run. Capability based security model…
I wasn't able to google it, or find a public link to the email (but it was posted on a public list) so here is some relevant snippets from it. Nov 20 2022 titled CapROS status "When I retired a year ago I hoped to…
Yeah, I did see a email on a capabilities list from him about him no longer working on it because of lack of feedback & wanting to just enjoy his retirement. That was the impression I got. When he had resumed his work…
I'd also note capros doesn't fit that description either. I don't know that there were examples that ran more than a single process. That's probably not true, for anything relying on drivers since user mode drivers are…
I wish he had just said 50 years of LCF, since he even mentions automath in the article but that was but that was late 60s
Presumably since this language isn't C they can define it however they want to, for instance in rust std::i32::MIN.wrapping_sub(1) is a perfectly valid number.
that all integers are either even or odd, and that for an even integer that integer + 1 and - 1 are odd and vice versa for odd numbers. That the negative numbers have an additional digit from the positive numbers…
Without the low int the even/odd theorem falls apart for wrap around I've definitely seen algorithms that rely upon that. I would agree, whether error values are in or out of band is pretty context dependent such as…
Seems doubtful, given that generics and the gccgo compiler were both spearheaded by Ian Lance Taylor, it seems more likely to me that him leaving google would be a more likely suspect, but I don't track go.
> * With a great non-political community (actually, this is the biggest lie of all). I recall the opposite, that the rust language (before the foundation) position was that being apolitical was a political stance. This…
The thing I love most about wezterm is the `wezterm cli list --format json`, and being able to get various values like the cwd of any terminal by window id. While I don't much tweak my actual wezterm config at all. I…
What I find funny about your argument is how completely degraded fair use has become when using anything by a corporation capable of delaying and running up legal fees. It sure feels like there are a separate set of…
It is fine though if people who don't knit enjoy knitting podcasts, but this is not that. Somewhere between the producer/consumer relationship there should exist some actual knitting. Otherwise (in cases like this) it's…
I'd also say a few things, if knitting takes a long time consider how long it takes to make a good clear pattern so that others can replicate it. People who make patterns are already dealing with a saturated market.…
Seriously? You can't get the feeling of satisfaction of wearing something, or having someone wear something you made from AliExpress. My point is your sense of feeling and validation is extremely distorted if you have…
Can't wear feelings and validation...
My only complaint with the article is that it doesn't seem to mention that digitized proofs can contain gaps but that those gaps must be explicit like in lean the `sorry` function, or axioms.
In FCC DA 26-68 they gave public notice of their change of interpretation/enforcement of the equal time rules to apply to this situation.
Maybe it can be done, but I struggle to believe adding in that branch for every forall quantifier (which may be plentiful in a proof) is going to help make a proof more understandable. Rather I feel like it'll just…
Rhetorical sentence? My point is that back-translation into natural langauge is translating into a less precise form. How is that going to help? No number of additional abstraction layers are going to solve human…
why do we invent these formal languages except to be more semantically precise than natural language? What does one gain besides familiarity by translation back into a more ambiguous language? Mis-defining concepts can…
> Proprietary use, commercial redistribution, or publishing modified versions with ads or tracking is strictly prohibited under GPLv3 or later. These all sound to me like "Further restrictions" which the GPL says: > If…
I feel like another optimization that rust code can exploit is uninhabited types. When combined with generics and sum types these can lead to entire branches being unreachable at the type level. Like Option<!> or…
I always feel that when saying lex/yacc style tools, it comes with a lot of preconceived notions that using the tools involves a slow development cycle with code gen + compilation steps. What drew me to the grmtools…
I would also say there is a 3rd class, which are distributed capabilities. When you look at a mobile program such as the GadgetBridge which is synchronizing data between a mobile device and a watch, and number of…
I couldn't agree with you more, the thing is our underlying security models are protecting systems from their users, but do nothing for protecting user data from the programs they run. Capability based security model…
I wasn't able to google it, or find a public link to the email (but it was posted on a public list) so here is some relevant snippets from it. Nov 20 2022 titled CapROS status "When I retired a year ago I hoped to…
Yeah, I did see a email on a capabilities list from him about him no longer working on it because of lack of feedback & wanting to just enjoy his retirement. That was the impression I got. When he had resumed his work…
I'd also note capros doesn't fit that description either. I don't know that there were examples that ran more than a single process. That's probably not true, for anything relying on drivers since user mode drivers are…
I wish he had just said 50 years of LCF, since he even mentions automath in the article but that was but that was late 60s
Presumably since this language isn't C they can define it however they want to, for instance in rust std::i32::MIN.wrapping_sub(1) is a perfectly valid number.
that all integers are either even or odd, and that for an even integer that integer + 1 and - 1 are odd and vice versa for odd numbers. That the negative numbers have an additional digit from the positive numbers…
Without the low int the even/odd theorem falls apart for wrap around I've definitely seen algorithms that rely upon that. I would agree, whether error values are in or out of band is pretty context dependent such as…
Seems doubtful, given that generics and the gccgo compiler were both spearheaded by Ian Lance Taylor, it seems more likely to me that him leaving google would be a more likely suspect, but I don't track go.
> * With a great non-political community (actually, this is the biggest lie of all). I recall the opposite, that the rust language (before the foundation) position was that being apolitical was a political stance. This…
The thing I love most about wezterm is the `wezterm cli list --format json`, and being able to get various values like the cwd of any terminal by window id. While I don't much tweak my actual wezterm config at all. I…
What I find funny about your argument is how completely degraded fair use has become when using anything by a corporation capable of delaying and running up legal fees. It sure feels like there are a separate set of…