ratmice

Feels like a hundred years later we're still cursed by the cocaine addiction of Dr. William Stewart Halsted

I wasn't really talking about just rings, the comment I was replying to was talking about heart rate sensors. I'm saying it's still worthwhile replacing your ring with a watch.

Even if it is just for swiping or pressing buttons to switch between exercises in your program. But there are other uses for accelerometers.

I wasn't wading into the watch/ring debate, never used a ring just a watch. Was just saying while heart rate data might not be the most useful. There might be uses for other sensors and reasons to replace the ring with a watch while lifting...

Not really the point.

If you make program with a bunch of different exercises, and are modifying your program a lot, it can be a pain to keep track of what your next exercise should be.

If you are automatically tracking reps, it can just announce whatever the next thing in your program is, and start rest timers automatically...

It's not really about tracking reps as much as tracking where you are in a program that it is useful for...

The data should be useful for automatically counting reps...

Perhaps it refers to PhantomData<!> but I don't know

Boxed slice isn't really the most well known type/optimization, There usually aren't that many vec's that it makes a big difference.

> We do not grant access to our license plate readers to federal law enforcement.

That sounds very weasel worded, if they get license plate readers from someone who does.

Thats not the point, if there were a better proprietary engine stockfish would still be there as a baseline. Anyone can access an engine as good as stockfish to practice against. Are any open models touting mathematical breakthroughs?

Another noteworthy difference is that Stockfish is also gpl.

It would be nice if OP noted what caused the change in their opinion?

did datafusion gain some feature that they noted was missing in the previous article, or did something in their understanding click so they could overcome the previous issues?

What I was (badly) trying to express was more that given static bounds rust could also eliminate dynamic checks. So saying e.g. ATS can eliminate static checks, is kind of switching the target.

those are not dynamic bounds.

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 just plain exploitation.

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. This includes historical/vintage patterns, which for many years patterns were primarily given away freely to incentivize yarn sales, or dominated by publishers. It wasn't until recently (internet, etsy, ravelry) when designers actually had the means to sell directly to consumers. People making an effort to produce usable patterns are now being dwarfed by AI nonsense in the speed of their output. It was already a difficult market. That everybodys images of real objects (along with AI generated ones) are being used to peddle and market patterns that will never work can be really demotivating.

One last thing is how many of the 8 people in this podcast company are actually generating slop and how many are actually just doing marketing?

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 no knitted material to show for it?

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.

Definitions are built up layer upon layer like an onion too, with each step adding it's own invariants reducing the problem space.

I just feel like the street light example is an extremely small free standing example. Most things that I feel are worth the effort of proving end up huge. Forever formal verification languages were denigrated for being overly rigid and too verbose. I feel like translations into natural language can only increase that if they are accurate.

One thing I wish is this whole discussion was less intertwined with AI. The semantic gap has existed before AI, and will be run into again without AI. People have been accidentally proving the wrong thing true or false forever and will never stop with our without AI help.

At the very least we can agree that the problem exists, and while i'm skeptical of natural language as being anything but the problem we ran away from. At least you're trying something and exploring the problem space and that can only be cheered.

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 balloon the number of words necessary to explain the proof. Feels like it's going to fall on the bad side of verbosity as the sibling comment said.

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 confusion.

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 be extremely subtle, if you look at the allsome quantifier https://dwheeler.com/essays/allsome.html you'll see that these problems predate AI, and I struggle to see how natural language is going to help in cases like the "All martians" case where the confusion may be over whether martians exist or not. Something relatively implicit.

Sure, in the Result case, less in the option case. I didn't mention it because Infallible is documented and named specifically as an Error "The error type for errors that can never happen". The use of uninhabited types as an unreachable code optimization is useful beyond errors though.

The sum of the note and the gpl doesn't behave as though the notice has any precedence over the gpl. It behaves as additional restrictions and a license that allows you to ignore the additional restrictions. I'm no lawyer but it seems like it isn't achieving what you want.

> 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 the Program as you received it, or any part of it, contains a notice stating that it is governed by this License along with a term that is a further restriction, you may remove that term.

It seems like if you want those clauses that GPL doesn't seem like the license you want?

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 Result<T, !>, rust hasn't stablized !, but you can declare them other ways such as an empty enum with no variants.

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 (eventually contributing to it) was that you can evaluate grammars basically like an interpreter without going through that compilation process. Leading to a fairly quick turnaround times during language development process.

I hope this year I can work on porting my grmtools based LSP to browser/wasm.

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 permissions it requires like contacts, bluetooth pairing, notifications, yadda yadda the list goes on.

Systems like E-Lang wouldn't bundle all these up into a single application. Your watch would have some capabilities, and those would interact directly with capabilities on the phone. I feel like if you want to look at our current popular mobile OS's as capability systems the capabilities are pretty coarse grained.

One thing I would add about compilers, npm, pip, cargo. Is that compilers are transformational programs, they really only need read and write access to a finite set of input, and output. In that sense, even capabilities are overkill because honestly they only need the bare minimum of IO, a batch processing system could do better than our mainstream OS security model.

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 will fix that.