apatil

I have found myself legit using this instead of duolingo for the past couple of days, in spite of the speech to text issues. It feels like a better way to learn. The inline suggestions, in particular, seem like they will help me quickly move through bad habits and mistakes in order of severity.

The tutor review at the end of the lesson doesn't feel as useful currently; its content isn't particularly actionable. Maybe if it gave me a couple of exercises or something?

The auto submit slider doesn't work for me (on Android) but I can imagine what it would be like. I don't think the Portuguese speech to text is good enough for the app to be usable hands free even if the slider did work. For example, it just transcribed

"Eu quero ir a assistir ao filme." (which is almost correct)

as

"Eu quero ia AA chistian ao filme."

These errors have to be corrected by typing.

I've used chatgpt itself as a language tutor a bit but this is nicer. I like the inline suggestions that don't break the flow of conversation.

Portuguese speech to text is flaky. This may be partly attributable to my pronunciation, and chatgpt has the same issue.

I'd love to have a hands free mode that's suitable for use while doing chores or driving.

Penalizing a crime might make sense for the purpose of deterrence even if there is no conscious free will. The size of the deterrent effect is a scientific question, and how to weigh the benefits of deterrence to society vs. the harm the punishment inflicts on the criminal is a moral question (where by moral I mean "should we do this").

However, penalizing a crime for the purpose of retribution makes no sense if there is no conscious free will. The criminal's consciousness experiences the harm of the punishment, but didn't cause the actions that constituted the crime. This is patently unfair.

I don't think conscious free will exists. One of the reasons I care is that, if most people shared that belief, we would talk and think about crime so differently that our approach to crime would change in the direction of becoming more humane.

For example, given the news of SBF's conviction for fraud, no one would be happy about the fact that he will likely experience many years in prison. We might be happy that the harm his actions caused has been stopped, and we may feel a kind of dutiful satisfaction in the knowledge that the system is working to deter and prevent this kind of harm. However, these emotions would be tempered by regret that a young man is going to lose part of his life, and we would be questioning whether there's any way to achieve the same level of harm prevention without inflicting such serious harm on one person.

I find it plausible that it's often a good idea in medicine to be conservative before launching interventions that may have adverse side effects, but have difficulty swallowing the idea that this conservatism should be implemented by reducing visibility (eg by not applying tests too broadly if they have a nontrivial false positive rate and the condition is rare). It seems like the right thing to do would be to maximize visibility, but then to try to corroborate and not overreact to apparent positives.

I heard about this video from an astronomer friend a few months ago. It was mostly about how Loeb's social and professional behavior matches with that of past crackpots. He does seem to leave himself open to that.

There wasn't really a material argument against his controversial hypotheses about interstellar objects. I counted an ad hominem (45 minutes of analysis of his awkward public persona), an argument from ignorance ('Omuamua is out of view so it's not possible to collect evidence for the lightsail hypothesis) and an appeal to the authority of the broader astronomical community.

He is going out and looking for evidence about IM1, and is seeking cross-validation from other labs, in a very transparent way. He's making lots of possibly inappropriately optimistic public speculations in the meantime, but I haven't seen him make any actual claims that aren't justified, which seems like the defining feature of a crackpot.

This makes sense, thanks. However, it doesn't mean that the 3% estimate of the chance of impact was wrong at the time of initial observation given data available, and that still makes it a huge deal at that time. At minimum, it would seem to justify using the best available instruments to characterize the asteroid more precisely as soon as possible.

If these large numbers happen so often that asteroids with initial impact probabilities of 3% are known to actually impact much less frequently than that, then the model is poorly calibrated, no? In other words, the reported probabilities aren't really probabilities and that is what has caused the confusion and anxiety in these comments.

Also, is it possible to quantify the risk of unseen companion asteroids, which someone else mentioned in the comments.

Two questions for people who live in rural areas in homes that were built in a more modern way.

- Do you have issues with pests? More precisely, how often do you have to use mousetraps or call an exterminator?

- What's your recurring home maintenance schedule like?

Two things that really bother me about American-style homes are the seemingly rapid deterioration and the failure to design out pests. It's easy for a stick-frame building to develop a defect sufficient to allow mouse ingress, and once inside, the hollow walls afford them many inaccessible places to nest. I really hate having to regularly kill, or at best relocate and traumatize, creatures that are just looking for a safe place to spend the winter. I have imagined that European-style concrete buildings, with tight-fitting prefab components, would be easier to own, but I have never actually asked anyone with a comparably located home.

Could anyone comment on how often Dafny finds proofs for useful theorems on its own in practice, without requiring the programmer to use expert knowledge of the proof search system to break it down into a sequence of gettable lemmas and/or refactor the code?

If the answer is "not that often", is there a possibility that LLM integration could help with proof search? This seems like an application where getting it 95% right is actually OK since proofs generated by the LLM can be automatically checked for correctness.

That's very interesting. In which variable is type inference EXPTIME complete?

Whichever variable it is, I suppose in practice humans can't create programs that are big enough in that way for type inference to become impractical. However, I wonder whether someone could comment on what this means about the utility of HM-like type systems in future AI generated software.

Sounds like an interesting story! I would love to see more sci-fi that really tackles AGI. I used to love sci-fi but most of it, even "hard" sci-fi, has become unwatchable or unreadable for me because the limited role of AGI is such an all-consuming plot hole.

I don't disagree, but I think the framing is overly pejorative and makes the likelihood of this outcome seem more tenuous than it really is. We do lots of things to help others because they make us feel nice. "Mothers and Others" by Sarah Hrdy argues that this tendency isn't just a fluke or a game-theoretic equilibrium of some kind between fundamentally self-interested agents, it's an ancient and deeply ingrained aspect of human nature.

The thought of living in a constructed world that exists by the grace of a single human owner of a super-powerful AGI is distasteful, of course, especially if the human owner uses their power to impose some of their own opinions about how people should think and behave. Becoming dependent on AGI is probably inevitable at some point, but I don't see that as so different from the status quo. We're already dependent on systems created by other humans that are so complex and sophisticated that no individual can grok them all.

I guess I would like to think that we will move past any initial impulse that the owner of the AGI feels to control other humans. We will presumably change so much that old ideas about how we should think and behave will seem irrelevant and quaint. And the AGI, which presumably will have the social engineering superpower, will hopefully point out inconsistencies between the owner's desire to control human thought and behavior and their desire for humans to live their best lives. Hopefully.