not serving this company has a very small effect on them

It has a big effect, instead. On the system. On their employees. On your employes and your customers…

Capitalism fosters a funny belief through its propaganda (aka marketing): that humans’ goals are always individualistic and social improvements always come from collective fights. This contraddiction (deeply internalized as many other disfunctional ones) fool many people: why be righteous (whatever it means to me) if it doesn’t change anything to me?

It’s just a deception, designed to marginalize behaviours that could challenge consumerism.

But if you cannot say “No”, you are a slave. You proved to be not.

And freedom is always revolutionary, even without a network effect.

Sounds like it was https://www.wired.com/story/palmer-luckey-anduril-border-wall/ ? Palantir at least has some positive clients, like the SEC and CDC.

It wasn’t. But the quip implies that we can act like a village, when the sad truth is that the low barrier to entry in software development means we can’t really act like a village, and stop people with our skillset from putting vile stuff into code.

There is, and I’m slowly working my way through it to write a blog post. THis is way more interesting as an introduction to model checking compared to the usual examples of the rower with the dog,duck, and sack of corn.

I haven’t had the problem the quote implies. The basic, type systems were about enforcing specific properties throughout the codebase and/or catching specific kinds of errors. They seem to do that fine in any language designed well. When designers slip up, users notice with it becoming a best practice to avoid whatever causes protection scheme to fail.

Essentially, the type system blocks some of the most damaging kinds of errors so I can focus on other verification conditions or errors it can prevent. It reduces my mental burden letting me track less stuff. One can design incredibly-difficult, type systems that try to do everything under the sun which can add as many problems as they subtract. That’s a different conversation, though.

This set includes programs that could be put to pass a type checker, given that you put extra work into it, or use a specific type checker for them. Otherwise that set is empty: For every program you can construct such variation where the parts that do not type check are lifted outside from the realm of the type checker. For example. stringly typed code.

The recipe to construct a program that does not pass a type checker is to vary things that have to be invariant for the type checker. For example, if you have a function that loads a function, we cannot determine the type for the function that is produced. If the loaded function behaves like an ordinary function, it may result in a dilemma that you may have to resolve either by giving it some weird different type that includes the idea that you do not know the call signature, or by not type checking the program.

Analogous to the function example: If you define creation of an abstract datatype as a program, then you also have a situation where the abstract datatype may exist, but you cannot type the program that creates it, and you will know the type information for the datatype only after the program has finished.

And also consider this: When you write software, you are yourself doing effort to verify that it does what you want. People are not very formal though, and you will likely find ways to prove yourself that the program works, but it does not necessarily align with the way the system thinks about your program. And you are likely to vary the ways you use to conclude the thing works because you are not restricted to just one way of thinking about code. This is also visible in type systems that themselves can be wildly different from each other, such that the same form of a same program does not type in an another type system.

I think for the future I’ll try to pick up examples of this kind of tricky situations. I am going to encounter them in the future because in my newest language I’ll have a type inference and checking integrated into the language, despite that the language is very dynamic by nature.

There is some work involved in giving you proper examples, and I think people have already moved to reading something else when I finish, but we’ll eventually resume to this subject anyway.

There’s a few major problems:

• The infrastructure he’s advocating is serious work to implement with any sort of performance, if it could be done at all on a world-wide scale.
• Any user interface cooked up by his teams over the years has been, ah… “not great”
• Most browsing / writing users will never need 99% of the functionality his structures give you, and will certainly never pay the price of the cognitive load those features bring with them.

But, those features (tracking transclusions, advanced versioning and two-way links, etc) would be super-useful for source code, and programmers are the kinds willing to give up some ease of use for power- I mean, most of us use git, and some weirdos even like it.

Edit: Additionally, when limited to an individual or limited group of codebases, the performance issues could be solved over time as the software was applied to larger corpuses (corpii? I dunno)

Because Nelson thinks that the links should never get invalidated by a single end point, and because he thinks that nothing in the system should ever be copied, but always linked to or transcluded.

When I was an undergrad, I relied on AFS and FrameMaker for a lot of assignments, and that was precisely how I collaborated with other students.

It worked for some things. BUt it’s part of why AFS didn’t become the Web.

The documents being annotated don’t know about the annotations. Nobody would see any annotations unless they checked for them. The same is true with hypertext.

Thanks, this made it click.

You can’t conclude that someone would not have stopped in time from the video. Not even a little. Cameras aren’t human eyes. They are much much worse in low visibility and in particular with large contrasts; like say those of headlights in the dark. I can see just fine in dark rooms where my phone can’t produce anything aside from a black image. It will take an expert to have a look at the camera and its characteristics to understand how visible that person was and from what distance.

From the video I don’t think a human would have stopped in time either, but Uber’s car isn’t human.

Certainly not when distracted by a cell phone. If anything, this just provides more evidence that driving while distracted by a cell phone, even in an autonomous vehicle, is a threat to life, and should be illegal everywhere.

The car does not share any responsibility, simply because it’s just a thing.

Nor does Uber, which again is a thing, a human artifact like others.

Indeed we cannot put in jail the car. Nor Uber.

The responsibility must be tracked back to people.

Who is ultimately accountable for the AI driving the car?

I’d say the Uber’s CEO, the board of directors and the stock holders.

If Uber was an Italian company, probably the the CEO and the boars of directors would be put in jail.

Not blaming the victim here

People often say this when they’re partly blaming the victim to not seem overly mean or unfair. We shouldn’t have to when they do deserve partial blame based on one fact: people who put in a bit of effort to avoid common problems/risks are less likely to get hit with negative outcomes. Each time someone ignores one to their peril is a reminder of how important it is to address risks in a way that makes sense. A road with cars flying down it is always a risk. It gets worse at night. Some drivers will have limited senses, be on drugs, or drunk. Assume the worst might happen since it often does and act accordingly.

In this case, it was not only a four lane road at night the person crossed: people who live in the area on HN said it’s a spot noticeably darker than the other dark spots that stretches out longer. Implication is that there are other places on that road with with more light. When I’m crossing at night, I do two to three things to avoid being hit by a car:

(a) cross somewhere where there’s light

(b) make sure I see or hear no car coming before I cross.

Optionally, (c) where I cross first 1-2 lanes, get to the very middle, pause for a double check of (b), and then cross next two.

Even with blame mostly on car & driver, the video shows the human driver would’ve had relatively little reaction time even if the vision was further out than video shows. It’s just a bad situation to hit a driver with. I think person crossing at night doing (a)-(c) above might have prevented the accident. I think people should always be doing (a)-(c) above if they value their life since nobody can guarantee other people will drive correctly. Now, we can add you can’t guarantee their self-driving cars will drive correctly.

In reality, both the pedestrian and the car (and Uber) share some responsibility.

I’ve also seen it argued (convincingly, IMO) that poor civil engineering is also partially responsible.

Yes, I document everything along the way. I do not like to publish about ongoing projects as I tend not to finish them when I do that :).

Both the code and the CAD designs will be open sourced once the project will be finished.

I also plan to write a proper blog post about it. I still need to figure out the proper way to do partial refresh with this screen and it should be more or less done (the wooden case still needs some adjustments).

[Edit] Typos.

Same, I would definitely be interested in following the project progress.

It seems to be this one, same marks on the bottom corners and the shield looks the same:

https://www.waveshare.com/wiki/7.5inch_e-Paper_HAT

Entirely agree with you.

I guess it can be explained by the fact that LCD screens have a better brightness, they are better to catch human eye attention.

The eink technology is bistable on the other hand, making it highly energy efficient for such applications - when no frequent updates are needed.

Energy is cheap nowadays, we don’t really care about energy consumption anymore. But I guess this might change past the peak oil.

I guess these techs will start developing as soon as energy becomes scarce and expensive.

No. THe only idiot I see in Rust is me. I meant idioms.

They’d be the ones out of habit trying to profile the garbage collection of their Rust app, gripe about standard library’s pervasive lack of referential transparency, or insist Simon Peyton Jones does a talk on every new feature. That I haven’t seen these people doesn’t mean they don’t exist. ;)

It’s on my laptop and I have Daniel Jackson’s book. Agda, Alloy and TLA+ are what I’m concentrating on.

The system is not Luigi… it’s an ad hoc thing built around APScheduler… We need decide whether to invest more effort making that work for a bit or look into the best way to move toward something else. It’s an interesting problem!