I do believe she eventually grows to the age of consent, but I could be wrong.
Of course, I was saying "only female" is Sassette erasure. I was not saying "only mating prospect" is Sassette erasure.
I was just remembering her from my childhood. I wasn't up on my Sassette lore. I found a reference that says she was created the same way Smurfette was, which surprised me.
I don't think that's right. The average voter wants the minimum wage raised by quite a bit. Capital voters paint nightmare pictures no matter how small the increase is.
Sure, eventually, I'd like a language with Haskell-ish syntax to compile to Linux x86_64 and webassembly and use the language to make better software. If my language existed today, I'd probably work on writing my own ActivityPub software, and improve/port https://github.com/NARBEHOUSE/Ben-s-Software- because my father might want it soon.
https://gitlab.com/bss03/grtt is my published code. But, I have far more intuitions that I need to write code for than finished code.
While evaluating something well-typed under a context, the heap: does not need to contain a value for a binder with modality 0, must contain a single, strict value for a binder with a modality 1, must contain a single, lazy closure for a binder with a modality of ?, must contain multiple references to a shared, strict value for a binder with a modality n, must contain at least a single reference to a strict value for a binder with a modality of +, must contain at least a single reference to a lazy closure for a binder with a modality of *. Since the typing rules propagate the modalities to subterms precisely, we should be able to identify the exact point a closure must be forced to a value (or dropped) before runtime. That's in addition to being able to compile linear functions to heap updates, eliminating at least some allocations.
There's some similarities with both the exact-use-count and relevant-or-erased semirings, but I think some things (e.g. around sums) are hard/awkward/impossible to type and the ?/+/* modalities make some make things easier while still allowing the abstract machine to know exactly when to "optimize the heap" based on a runtime flow that "activates" a particular static analysis.
Of course, it's still MLTT "compatible" -- anything that would type-check in MLTT should type-check in my variation of GRTT by "simply" using the * modality everywhere -- so you get full proofs-as-programs and a total language.
I'm probably a bit off in the weeds, but it still makes my brain buzz to think about and occasionally I'll make progress. I've been a little bit distracted with https://gitlab.com/bss03/nested which should allow me to write the abstract machine as a fold, but as proven to be place I can also put a lot of programming time into (again, with sporadic real progress).
I think co-ops are the way to go, but I can understand that someone "just" wanting to purchase the good/service might not see the difference between a co-op and corporation like Amazon.
I don't think it's a size issue really, but co-ops generally stay smaller in part due to how they are internally organized compared to a "median" corporation.
I also think that the government actually does a pretty good job at managing things; it's just their failures are public. Private boondoggles might drive many people into bankruptcy, but they aren't publicized any more than absolutely necessary.
I think "graded" in the name is there in contrast to "quantitative" type theory, which doesn't have modalities/quantities at the type-level.
The "modal" is borrowed from modal logic. If you pick the correct semiring, you can recover linearity and affine-ity and the other substructural logic pieces.
The quantitative semiring I've been working with is 0, 1, ?, n, +, *, which I think will let me use static analysis to do very precise non-strictness and precise/early resource tracking/release. (But, my progress is so slow, that if this were an academic project, I don't think I'd be getting any more grant funding.)
I don't think copyright is currently serving it's purpose "To promote the Progress of Science and useful Arts". And it should be eliminated anywhere it is not doing that.
Closest to my pocketbook is software (I'm a programmer), and I think we'd almost certainly be better off without copyright of any kind on software. It would mean exercise of some of our freedom around software would have to be implemented via reverse engineering, but it would make that route much more available / less risky for software that is current not Free Software. But, maybe I'm extra jaded because software is almost always done as "work-for-hire" so the author doesn't actually hold the copyright, the Capitalist employer does.
I agree that John was the problem, but I think it was management responsibly to fix. Either through some coaching or as you say, before he became business-critical.
Rice's Theorem prevents this... mostly.