grumdan

A standard state machine with no memory (other than the current state) is equivalent in expressivity to regexes (in fact regexes with back-references are more expressive); even if the state machine is non-deterministic.

I think one of the things that makes HN and Reddit very different, is that the content is not personalized and tailored to maximize user engagement. Facebook seems to constantly show me things that make me more upset or concerned or outraged about something. I remember reading articles documenting this effect, but I can't seem to find them now.

The other type of posts I tend to see are about friends bragging about how many km they ran today or how great their vacation was. Not that it's that bad to post these things, but I wouldn't be surprised if exposing yourself to them constantly increased feelings of jealous and reinforce one's need to compare oneself to others.

On the other hand, I've discovered a lot of interesting books and projects through HN and learned about different topics, since there seem to be a lot of knowledgeable people here that comment on topics I know nothing about. The only type of posts that may be prone to making others feel worse are the ones about salaries / financial issues, but they are not that common.

This complete speculation from my side, but I would think that playing video games themselves to be better (or less harmful) than just watching other players. If I had kids, I would be more likely to limit how much they can watch others play and let them play themselves more.

This is however hugely biased from having played a lot of video games as a kid and I felt it to be much more dynamic experience that may even help developing some mental faculties than passively watching anything.

> I agree with you that compositing/window manager fragmentation is a problem. And this article is a perfect example of that. The author may think that they're happy using i3 with Firefox and st at the moment, but the desktop computing environment has gotten so complex and the expectations of users who interact with desktop applications so rich, that a small hobby project DE/WM cannot fully satisfy all of those use cases over the long term.

Users have different needs and preferences, so I see the fragmentation as a positive thing because it gives people choice.

For me personally, xmonad, one of these hobby projects, has been perfectly sufficient for the last 10 years. I also didn't really touch my configuration much in the last ~8 years. More importantly though, I find it actually reduces my mental workload since I no longer have to handle window placement myself.

Is it really important how easy it is to learn a language when we are talking about formally verified operating system kernels? Beginners are probably not going to write formally verified code, let alone formally verified system code, so this area is already only accessible to veteran programmers who may not have a problem with these aspects of Rust.

I don't think it's a contradiction to introduce people to programming with more "elegant" or uniform languages that are closer to math (like Scheme or Haskell), or "easy" languages like Python, and then have them move on to Rust if they want to do system-level programming.

That's true, though at this point against a sophisticated attacker, it might be game over anyway, since they could read out the encryption key from RAM directly if it's still turned on. If the device is off, the fingerprints won't help and the data is protected by the long passphrase.

Of course all this assumes a particular attacker model and for a lazy attacker that doesn't know how to use the fingerprints to fool the sensor, everything is fine.

Another downside is being possibly forced to unlock my phone at airports, since as far as I'm aware, passwords are protected by the fifth amendment whereas fingerprints are not. In this case it might be smarter to turn off one's phone entirely when crossing borders into countries where one can be compelled in this way. This doesn't even go into all the other kinds of pressure they might apply to make me unlock my phone anyway though, so there's not much protection here aside from leaving my good phone at home.

While biometric authentication is overall less secure and can be circumvented, I still think there are situations where it's preferable to the alternatives, in particular on smartphones:

All Android versions I used don't support setting an encryption passphrase that's separate from the unlock pin/password. As a result one has to choose between a very long unlock password one has to enter all the time or a convenient short one making encryption basically useless. Given this trade-off, I think using a proper, long passphrase for encryption with a fingerprint for normal unlocks is preferable to the alternatives. It's particularly irritating that this restriction is not at all technical; the only justifications I've read were along the lines of "it might confuse users".

Less importantly, for my phone, a shoulder-surfing attack seems much more likely to me than someone specifically copying my fingerprint.

I would go further than that and say that it's also important for programmer to know different paradigms. Knowing C, Java, and Python is surely better than just knowing Java, but they're still quite similar. Ideally people would also learn some functional programming, even if they don't use it, and a Lisp dialect (to appreciate the value of good metaprogramming facilities and get over parenthesis-phobia).

It's not a specification, but an interesting project is to formalize and prove safety guarantees of Rust:

http://plv.mpi-sws.org/rustbelt/#publications

In order to do this, there also needs to be an unambiguous formal semantics of Rust, so one might even hope that this will turn into some form of official language specification.

> In the case of Patreon, there is a man who people want to give money to. He wants to accept that money. There is no criminal activity on either side of the transaction. Yet Patreon is preventing these people from doing what they want because Patreon dislikes one paragraph of the man's boorish utterances.

Patreon isn't "preventing" the transaction, they are merely choosing not to facilitate it. Respecting individual rights does not oblige anyone to help others to do what they want to do.

This would still be consistent with there being genetic (or otherwise hard to change in adulthood) factors that make a person function better with a shifted sleep cycle. It's not at all clear that it's all environmental (like the post I replied seemed to imply) and I find it irritating when people make such sweeping claims without evidence.

> Sleep cycles exist and aren’t innate. Your engrained behavior or schedule is something that sets your cycle, but is changeable.

How do you know this? Not trying to be snarky, I'm just wondering if you have any evidence for this claim.

It's important to note though that their client is not open-source, so if one goes through all that trouble to use end-to-end encryption, it seems a bit unsatisfactory to me to then trust this company to actually keep the private keys on my machines (and encrypt things correctly).

Personally I used syncthing which doesn't do encryption but also only uses my own devices, so I can keep the data on my machines at all times.

In the past I used seafile which does support encryption (and it's self-hostable): https://www.seafile.com/en/home/

To be clear though, all the mentioned languages are built on purely functional programming. Coq and Isabelle are more "procedural" in that they include special proof languages that express proofs in a step-by-step way that feels procedural, but the programs and definitions one proves properties of are still expressed in a functional style.

It's true that one needs to prove a lot of trivial things in all these systems, but the extent of this varies dramatically based on how much automation they provide. For example, Agda includes only minimal, barebones proof automation, while both Isabelle and Coq allow using more sophisticated automation that can take care of a lot of trivial steps automatically (such as "x == x").

In addition to Coq that other commenters mentioned, there is also a family of proof assistants based on higher-order logic. Isabelle/HOL[1] is probably the most widely used prover in this family, which also provides a great deal of automation compared to other provers. For example, it has been used to verify the seL4 microkernel [2]. As for introductions to the topic, I can recommend "Concrete Semantics" [3] which introduces the reader to Isabelle/HOL generally and shows how to model semantics of programming language and prove properties about them.

For Coq, a widely used book to get started is Software Foundations [4] which is also focused on PL semantics.

[1] https://isabelle.in.tum.de/

[2] https://sel4.systems/

[3] http://www.concrete-semantics.org/

[4] https://softwarefoundations.cis.upenn.edu/

Haskell (in the form of intero+emacs at least) also has very nice REPL integration and will automatically reload any changed modules and any modules that depend on the changed modules. The debugging facilities are nowhere near what CL/SLIME offers, but I find I need a debugger much less often in Haskell anyway.

Some model checkers are bounded model checkers, for example CBMC, a bounded model checker for C. In practice this sometimes means they only unroll loops a certain number of times, so they might miss assertion violations occurring in later iterations of a loop. You're right though that there are model checkers that are not bounded and these do provide guarantees.

The Mind Illuminated by John Yates (aka Culadasa) helped me a lot on how to structure my practice and how to deal with specific issues arising during meditation. I also find it quite well-written.

Technically true, but the quote makes it sound as if this were not necessarily the case for some kinds of exponential growth, which is clearly false.

Haskell is being used for their spam filtering system, Sigma: https://code.fb.com/security/fighting-spam-with-haskell/

I'm not sure what else they use it for, but they hired Simon Marlow, one of the main guys behind GHC a years ago. It's still not their primary language, but restricting the interpretation of "professional" and "uses" to what you had in mind is not the most interpretation of your comment to me.

> why not something used by literally any professional company

Can we cool it with using "literally" to mean "figuratively"? You may have heard of Facebook or Standard Chartered for instance, unless you consider them both unprofessional. Sure, it's less common than other FP languages, but Haskell is used for non-trivial things by non-trivial companies.

I think it's a matter of taste. I find seeing boot messages about services starting up etc. more aesthetically pleasing than some logo. It reminds me of people who buy mechanical watches where the gears are visible. Seeing the underlying bits of a complex system exposed can certainly be appealing to some people.

While I agree that a certain base level of income is necessary to have decent life, it becomes a lot less important after that's reached. And that level for me mostly includes enough money for food, accommodation (, and healthcare if you're in the US) and some extras like going out or traveling once in a while. In Europe this is pretty easy to achieve in a technical field. Beyond that, I feel like more money doesn't add much to my happiness. Saying that this is one's most important asset sounds like one should spend most of one's life on maximizing income, which I think is indeed a bit sad.

These are good reasons for why people might prefer python over other imperative languages, though basically all these points also apply to Haskell/OCaml/F#/etc., though some people would still say that a lot of things there look like line noise.

I think the GP's point was that functional languages give you similar benefits, but with more uniform and disciplined behavior of many language features. Why FP is not more widely used compared to imperative language is another topic though.

Isn't this only disturbing if one rejects there being an objective distinction between misinformation and information? Sure, there are gray areas, but there are many actors exposing people to indisputably factually false claims, and "false" in this sentence is quite often not a political concept or subjective. The pope didn't endorse Trump. Trump's inauguration crowd was not the largest in history, etc.

Google may be involved in a lot of manipulative things, but trying to distinguish between blatantly incorrect sources of information and the rest does not seem like a shady political motive to me, and there overall goal seems worthwhile to me. Encyclopedias and scientific journals also manipulate what people are seeing and I don't think filtering mechanisms in general are problematic; it depends on how the information is selected, and if this is done through a good process, it can be very beneficial.

I would also expect people's propensity to take screenshots to be correlated to how sensitive the image is. For example, I would expect many people to take a screenshot of a nude pic their partner sent just so they can look at it for longer than the default timeout of a snapchat message; this is even more likely for teenagers who may be less mature about not betraying the other person's trust.

One point of the article is that nobody is trying to take HTTP away from anyone. I'm not aware of anyone removing HTTP support, just a change to the UI that communicates what guarantees you don't have for this connection.

I think the overall quackery and use of bizarrely flawed and insane reasoning by charlatans is reminiscent of anti-vaxxers.

Additionally, I think use of HTTP over HTTPS could conceivably lead to actual harm for users unaware of the implications:

If for example commercial websites adopted the recommendations of switching to HTTP, people could actually lose money, so this may cause financial harm. Even worse, imagine, for instance, Facebook running over HTTP in an oppressive regime where, say, homosexuality was illegal; if this regime also didn't have enough clout to get Facebook to give them access to their data, then they could now more easily identify and persecute people for their communication content (same would go for dissidents or journalists if they used this), resulting in much worse harm to people than just losing money. There are many other examples were losing confidentiality or integrity of your communications can actually harm you, I just picked the first two that came to mind.

They are language-independent but may still have a higher incidence in one community than another. Anecdotally, these basic mistakes seem to happen more in Node packages or JS-based projects, but I have no concrete evidence for this speculation. The only study I know of looking at this in a serious way is this one:

http://web.cs.ucdavis.edu/~filkov/papers/lang_github.pdf (https://news.ycombinator.com/item?id=8558740)

However, JavaScript ends up a being less prone to defective commits than C++ and C, as well as PHP and Python, but there are a number of issues that don't allow us to conclude all that much from these results (imo).

I agree, though I prefer the word trust; I think in the end most security arguments basically move trust around between entities, so I would either trust the open-source community or Apple.

In this case I decided trust the open-source community more than Apple, since the incentives of people inspecting open-source code probably align better with my own interests than the incentives of Apple.