I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?
11,016 karma · joined August 5, 2014
I anticipate the apathy to continue, and the bill to be passed along as some form of regressive tax.
'within the historical record' -- No one still makes a big deal about it because it happened long enough ago.
There are places that are not widely contested today, generally most of their present borders are assumed to be generally stable. Or places with obvious natural geographic bounds and mostly internal conflict through history.
Yet at some point were those places not battled over? Even the internal conflicts count, even if as a whole the majority of a country's population of today considers themselves of one people.
The regions that remain in conflict are considered such largely because of the people who have, at some point, lived in an area long enough for it to become a notable part of their history, they have not unified as a people OF a place, but as a distinct ethnic group (be that religious or otherwise) who happened to have at some time lived in some area.
They have all been 'wronged', and all* (generally an assumption but likely to be true) have 'wronged' others (at least in 'aggressive self defense' if not in some other way) at some point.
-- put into a metaphor --
There's a public park owned by the people (earth) which has a single tree that many children have made memories with. However two or more groups of childhood friends want to continue making memories with that tree and disagree with each other and how each other interact with the tree.
What is the solution?
The evil answer from a fiction writer is to destroy the tree to remove the problem. However that does not make a right.
Using any method to give the tree to one group would be a wrong to the other groups.
The groups cannot agree on how to share, nor how to all be full adults and make memories with the tree in peaceful coexistence.
Thus, lacking an accepted answer, the problem remains unresolved.
All land, everywhere. It is NOT a natural right that anyone owns any land, nor that any countries exist. That is something everyone's ancestors fought each other for and created as a system of human society.
Of course that's written in the past tense. Facing reality rather than the fantasy presented in history books and documentaries; not only did our ancestors do that, it hasn't stopped. The bloodshed still happens today in so many places. Those we might hear about in the news, and others forgotten even in the news because it is considered normal and thus ignored.
We are not yet a species of plenty. Scarcity still exists, at the very least in the real form of land where people want to be.
The human factor adds knowledge of the why that refines the results. Not just any algorithm or a standard pattern that fits, but the correct solution for the correct question.
pgp as a tool could integrate with that, but in practice fails for... many reasons, the above included. All the other key exchange / etc issues as well.
I also believe an off the shelf example of how to use the library correctly will save everyone a lot of pain later.
Consider moving to micro-services only AFTER reasonable algorithms on commodity bare metal show real capacity limits. There's still higher spec bare metal to carry said designs through a refactor / expansion based on where the performance bottlenecks are. Even absent literal micro-services there's still partitioning / sharding which can spread out many of the pain points.
Oh and rootkit level EAC? Expect that to go away on Windows too when MS finally gets sick of Crowdstrike and that ilk causing self inflicted Denial of Service attacks on whole economic sectors.
When your life is set like that why risk trying to defraud someone a the cost of a nice suit when that's something that can be done legally and written off as a business expense on taxes?
E.G. Comcast should be REQUIRED to give my OWN router a /56 or better, not a /60 because they waste a whole nibble of netmask at the cable modem which will _never_ talk to anything other than Comcast or my own Gateway.
Adding an external sound card introduces variables outside of manufacture control, the quality, latency, and drive power all at the mercy of some random integrator.
My phone is easily thick enough to accommodate a 3.5mm port, and it can't be that difficult to waterproof such a jack, which should also make reasonable cleaning easy if it's ever required.
People change over time. People change even a little based on who's around them. Even memories change as people see things in new lights.
The Internet of the late 90s and early 2000s was spectacular in that everyone could be as authentic and deep as they wanted to be, and as shallow and invisible as they wanted to be depending on context.
Firefox? Want to know how to really sell yourself. Be 'For the User', like TRON (but avoid that for copyright reasons and because normal people don't understand). The user should be able to TRUST that Firefox isn't selling them out, spying on them, or doing anything strange. That when Firefox creates identity sandboxes they're firewalled from each other to the maximum extent; including resisting device fingerprinting (just look generic and boring).
I'm barely willing to tolerate Steam's default DRM a little. Those are 'just games' and that particular version doesn't try very hard, plus the rest of the package (network effect, servers, and a strongly customer friendly brand) combine to balance out the negatives. I'm generally hopeful that as things become classic Steam will either continue to maintain the access servers or release versions that work properly without them.
For static media, just give me a reasonable way to pay a reasonable fee for the use license and place to get an unencumbered official high fidelity copy to enjoy.
Paraphrased: 'Copyright infringement indicates a customer service failure.' At least with respect to anyone who'd have considered the purchase in the first place.
Where possible you want everyone to be well informed on the way in, at least about the current situation and the obvious proposals. This gives people time to digest the information and maybe even suggest their own proposals.
Then there's two types of meetings.
* Leadership communication meetings (quick review to make sure everyone understands how important the data they already knew about is / cement context).
* Brainstorming meetings (figure out a plan / pathfinding)
I am speaking of most of America, where that is NOT happening because densification of areas is blocked by those already nearby who like the way suburbs near jobs are. (I don't blame them, apartments and probably condos SUCK, the building codes don't protect me from the choices of those nearby so everyone suffers the most annoyance.)
In effect, I am encouraging at least some of those nearby areas to experience zoning upgrades. Like in a city simulator when low density residential gets replaced with high, and mid and high rises replace older single family homes and suburbs.
The people who can least afford to move closer to their jobs are the ones who are regressively taxed in time, energy, and money the most.
A proper solution would be to require more housing NEAR the jobs to make it easier for people to save time and money by moving closer.
Plain text and flat images are my preferred formats for things which must be redacted. Images require a slight bit of special care, as the example in the underhanded C contest highlights, but it's possible to enforce visible redaction and transcription steps that destroy hidden information.
Heck even a targeted but small percent increase in sporadic behavior for targets of high value might be a worthy harassment tactic.
* For hit movies buy an obscene number of copies to rent month 1
* Sell off some for a discount as the rentals dwindled
* Discount anything over a reasonable backlog / duplicates set shortly after
Offhand I think they tried to time this to end well enough before the release windows slid to TV + Ads distribution.
* Rent the backlog until dead or until they sold in a discount bin
Some independent shops also competed. I recall my parents kindly rented a few less popular games they happened to carry. Not sure about videos, might have been better for stuff not mainstream enough at the big national chain.
In some sense, early player pianos (IIRC with holes in paper that controlled key presses) weren't computers, but were a related precursor technology / infrastructure.
JSON's just a nightmare though. The inane legacy of UCS2 / UTF16 got baked into Unicode 8, and UTF16 escapes into JSON.