skysight-inc/HackerNews huggingface dataset:
Apple Maps thinks the Ferry Building in SF is six miles inland
I recently tried to meet a friend at the Ferry Building at the Embarcadero in SF. The address
is:

One San Francisco Bay Trail, San Francisco, CA 94111

When I texted that exact string to an iphone user, it turned it into an Apple Maps link. Tapping on the link sent her to a location more than six miles away.

I'd heard Apple maps had some issues but this seems ridiculous. Is this a common occurrence?
The Wayland Zombie Apocalypse Is Near
is the list only for FOSS?
https://lobste.rs/s/48ciw9/wayland_zombie_apocalypse_is_near
Fab, I remember this fella from years ago. There's a series of four videos on YouTube featuring him explaining and demonstrating his craft:

https://www.youtube.com/watch?v=5I9L1aF6kiM

https://www.youtube.com/watch?v=aT1RkaaKYOo

https://www.youtube.com/watch?v=ufhCDe1r_-c

https://www.youtube.com/watch?v=zLv4lErCupQ
A century of suffering in the Middle East, Africa, and Southeast Asia is the consequence of those little wars.
On at least some gas pumps, pushing the button on the upper right will mute the sound (the video still plays). I just heard about this a few weeks ago, and tried it at a Chevron station near my house. I can confirm that it works!
Why is it a problem to change the device every 15-25 years?
>> How would we get the nuke to the asteroid?

Oh, it's simple- we'd sent in Bruce Willis [1].

__________________

[1] https://en.wikipedia.org/wiki/Armageddon_(1998_film)
If you don't want to watch through the whole thing I wrote a post the gives an outline, see http://mattwarren.org/2017/11/14/Microsoft-and-Open-Source-a...
Hobby learning is different from professional learning. For hobby learning the projects can span over several years or more. It is supposed to pleasurable, there are no deadlines, and the topics can be very distant from what one already knows.

For professional learning, it is a bit different.
> Although we were using Elasticsearch in the beginning to power our in-app search, we moved this part of our processing over to Algolia a couple of months ago;

How many records are you storing on Algolia?
.NET Core does not have an implementation of WCF, and I can’t imagine to ever will.

.NET Core has a pretty good MVC framework you can build REST services on, GraphQL, or gRPC etc.

Most of the framework baggage was left behind.
> Because the specification can be just complex as the system

Can you give an example of this? I don't find this true in general at all e.g. writing the specification of a sorting algorithm is much easier than implementing most practical sorting algorithms.

> the proof can only provide a false sense of security. A correctness theatre.

You could use this argument to say that unit tests, type systems, code review etc. are correctness theatre. All these things prevent mistakes.
From the source: false, true, true, false, true, true, false, false, true, true, true, false, true, false (go left to right, top to bottom)
>I do recognise that the threat of an invasion by an alien super-civilisation is at almost as remote as the threat from an emerging superintelligence

Uh.. Is that something one can 'recognise'? (It's a way of writing that begs the question.) Seems to me the threat of the first is not high, to say the least, but who knows. The threat of the second seems very high, well, at least if there are only 'a few nukes' on the planet. Otherwise nukes will get us first. I literally can't imagine 'nukes getting us first' but it does seem likely.
Fred Brooks said it years ago: "Even perfect program verification can only establish that a program meets its specification. … Much of the essence of building a program is in fact the debugging of the specification."
I would assume that if you had no fan, then the only things that could “degrade” on a computer would be the battery, thermal paste, and the capacitors (and maybe the screen backlight in a laptop.)
Ask HN: Which Is Better for You and Why, Amazon Echo Dot or Google Home Mini?
I am trying to get some last minute discount gifts for friennds. One is a couple and the other a single lady. I am wondering which one would be better for either.

What has been your experience with either of these products and what sort of personalities do either suit best?
I think we agree, but I would say computers are used _more_ to crunch numbers. Inside the system, everything is binary; you only need decimal to present data to humans.

With old time COBOL workloads, a lot of the stuff you do was presenting stuff to humans. The typical banking application, for instance, reads numbers, does a few additions, and shows them on a terminal or prints a report. Using fixed-point arithmetic was normal.

Nowadays, we do way more floating point arithmetic (for graphics, for machine learning)

Also, I think the reason those complex instructions aren’t created anymore is pipelining. I can’t find timing information for the ED instruction, but I think it is a safe bet it isn’t constant cycle count, let alone single-cycle. It not only writes a character buffer, it also has to read the bytes containing the pattern defining how to format the number.
The issue is not the edge of logical independence, but rather how easily can you express certain theorems. Most verification is about the verification of programming languages (e.g. the POPLmark Challenge [1]), and in this setting sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily.

All that said, automation of provers based on the LCF approach with a non-constructive logic is much superior as of December 2017. With this in mind I was surprised to see that L. de Moura based the new Lean prover [2] on a variant of the CoC. He thinks that all automation that we currently have for HOL (i.e. Isabelle/HOL) can be brought to Lean.

J. Blanchette [3] seems to think the same.

[1] https://www.seas.upenn.edu/~plclub/poplmark

[2] https://leanprover.github.io

[3] https://people.mpi-inf.mpg.de/~jblanche
Dealing with any issue in the Apple community is mostly baffling. The mindset of it works for me just pisses me off so much. Got a weird apple bug? 20 comments of how it works for them and YOU must be the problem. Watching people do mental gymnastics to apologize for the battery slowdown issues on iPhone recently makes me throw my hands up in the air and land of my face.
There's also BaseCoin, another attempt at a "stable coin" with prominent investors:

https://www.coindesk.com/basecoin-revealed-a16z-metastable-s...
Why? It's true, and useful to know if we are talking about efficiency.
Show HN: MailTrigger – A Simple HTTP-Based Email Notification Service
I would be interested in your point if you were revealing something concrete about the OP and their research, but you’re just making handwavy claims about broad correlations (“empirical research” = “study suggests xyz”)

The fact that you’re making overly broad claims accusing people of making overly broad claims doesn’t instill confidence that you know what you’re saying. If you’re such a champion of science, why not state your claims minimally concrete terms. And ideally make falsifiable claims.
Who are these people trading with? People trading OUT of cryptos INTO fiat. How does the asset distribution change, net, in that exchange?
JMod: extensible toolkit for community detection in networks
What is the purpose of publishing information like this?

At best, it’s trivia, at worst it provides advantage to a rogue nuclear power with active concentration camps.
I guess - if you consider 30 year old legacy technologies insanely cool... Redshift is a shared-nothing architecture, so you'll always face scalability and concurrency issues. Snowflake is a brand new MPP shared-data architecture, and it can scale compute and storage separately. Blows Redshift away.
This blog post explains the motivation and design rationale behind this tool in some more detail:

https://bjoernkw.com/2017/12/24/mailtrigger-a-simple-http-ba...
> I wonder if the problem is bad source material/generational loss.

For VOY at least I suspect generational loss - for example, there is a noticeable Moire on Voyager's deflector dish in the intro.
Division is slow. I recently needed to send 16 bit integers over a UART and came up with something like this:

uint16_t n,d;

// 10K digit
d = ((uint32_t)n * 53687 + 8208) >> 29;
n -= d*10000;
// output d+’0’

// 1K digit
d = ((uint32_t)n * 2097 + 1368) >> 21;
n -= d*1000;
// output d+’0’

// 100s digit
d = (n * 41) >> 12;
n -= d*100;
// output d+’0’

// 10s digit
d = (n * 51 + 40) >> 9;
n -= d*10;
// output d+’0’
// output n+’0’

It does scale to 32 bits but will require 64bit intermediates.
Precise humans will turn it off and post elitist comments on internet forums.
We’re getting 90 TFLOPS on AWS V100 for deep learning (using dlib not Tensorflow), so I can’t understand this comment:

> With TensorCores the Titan V has a new shiny deep learning feature, but at the same time, its cost/performance ratio is abysmal.
What 'incredible claims about his capabilities' did he make? (I came in late.)
Because the specification can be just complex as the system

That's true in principle, but in practice I don't think it's going to hold in most cases. A good specification necessarily captures the essential complexity of the system, but it's a lucky developer whose implementation doesn't introduce considerable accidental complexity as well. Ensuring that this accidental complexity doesn't break anything could have great value, depending on the nature of the system and how damaging a failure could be.
Key compromise and root cert with exposed key in German lawyer software (beA)
As I said in my comment, problems like in this case can be addressed. And such problems don't argue against all forms of autocorrect like the comment I replying to was rallying against.
“While other payments networks typically charge the greater of ~3% and $0.15, Bitcoin’s transaction fee tends to be a negligible fraction of the transaction, if any at all.”

That article seems quite dated (2015). The fees and transaction times for btc today are much worse:

https://bitcoinexchangerate.org/fees
I would not recommend VB.NET to anybody. The similarly to VBA is only very superficial and otherwise pretty much all attention is on C#.
Why are big companies so inaccessible? It's a strange paradox to think that almost everyone uses Google services on daily basis, yet it is near impossible to communicate with Google itself.
This actually worked out for me! Thanks!
I think most kotlin teams would want you to already know Java, the parts of kotlin that aren't basically Java under the hood are likely very easy to learn.
The lucrative art of chicken sexing
To be fair: if you are being locked up, having your money in crypto isn't going to do you much good. Apparently Swiss banks have been working overtime to repatriate Saudi funds that have been held there for over 50+ years.
Serverless is just another word for "third party service".
So whose mouths should we trust and why? (Apart from yours)
Then it must be better for Apple to cripple old phones. /s
How big is your codebase for this to be a factor?
متى يهدم اليهود المسجد الأقصى.؟
Although the CompCert paper explicitly says that the parsing step, as well as the assembling/linking steps, are not verified, this kind of bug is a huge blow to the credibility of formal methods. It really makes you wonder what sort of bugs formal verification is supposed to catch.

That's strange I reach the exact opposite conclusion on this statement.
The problem is that people are trying to have different experiences at the airport.

Some people are trying to work, some people want to sleep, some people are reading or watching their own media. I'll sometimes go to an unoccupied gate if I need to make a phone call, since nobody wants to share that.
Bogus.

The map colors individual "blocks" that have a certain number of alleged providers, but I know in some cases that one provider is available on one side of the block and not the other.

Bogus map (and other lookup) sites that claim people have more internet providers than they really do have been a sad part of the underinvestment in broadband infrastructure. They give ammunition to politicians who say there is no problem because they see it is fine on the map.
> Is this true though? What program properties can Isabelle easily automate the proofs of that Coq cannot?

Almost all?

Granted, I haven't used Coq very much, so correct me if I'm wrong, but isn't it true that in Coq, with the exception of basic proofs like simple arithmetic expressions, in order to prove a theorem you have to at least explicitly know and write the name of the lemmas that are needed to prove it (apart from how they fit together)?

In Isabelle/HOL, many times you literally only need to write "try" and Isabelle will find the proof of the theorem for you, including the lemmas that were needed to prove it and how they fit together (assuming these lemmas were already proven before). If it turns out that your theorem is false, it can show you an example of inputs where it fails.

This auto-proof functionality I'm describing is mostly thanks to Sledgehammer [0], the auto-counterexample finding is due to Nitpick (and another tool which I can't remember), although there are a few other automation tools that are also very useful.

Granted, you still have to have a high-level understanding of how you want to prove your code, but I would argue this eliminates a lot of the work and (wasted?) time you need to accomplish the final goal...

[0] http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehamme...
Not necessarily. One can pick up Kotlin as entirely new language. If you are working with old Java code, then yes.
Yes, I saw that. I'm planning to make something similar, but still pretty different.
Please don't spam.
That's already happening. For example, see https://runtimeverification.com/blog/?p=496
I'm a C/C++ developer for 15 years. I'm planning to do this mainly for learning purposes, and to create my newest project (actually an umbrella project containing 5 different projects).
One example are nominal techniques [1]. While they are constructive, they have so far only found substantial implementation in Isabelle/HOL [2]. The reason is that the natural implementation is non-constructive, and leads to only a small blowup in proof complexity, which can easily be handled by Isabelle/HOL's proof automation. In contrast, constructive implementations of nominal techniques seem to require a considerable blowup in logical complexity, which the existing proof automation in Curry-Howard based provers doesn't seem to handle gracefully.

Another issue is that most of the automation that is known as "hammer" is based on non-constructive automatic provers.

[1] https://www.cl.cam.ac.uk/~amp12/papers/nomlfo/nomlfo-draft.p...

[2] https://nms.kcl.ac.uk/christian.urban/Nominal
OWASP, you keep saying that word. I do not think it means what you think
"Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize."
> Cutting terrestrial cables just requires a local guy with a map and some TNT.

The truth is much simpler, and less explosive, it's usually a JCB digger operated by the local water/gas/leccy company that causes mayhem.
This is like asking: "Which is better for you, crack or smack?" Both are terrible devices whose primary purpose is to invade upon privacy so that they can sell your preferences to advertisers.
It is possible to do this, you can get DWDM transmission equipment with encryption built in, I assume some submarine cable capacity purchasers make use of this, but is raises the cost by a decent amount.
The title is very misleading. This just talks about Earth coverage of missile launch detection system according to publicly available information. This has nothing to do with detecting submarines.
Great news! On a related front, I find it appalling that a $1000+ device that can map your face, tell you where you are and act as a real-time assistant renders unstyled HTML with absurdly tiny font size. (Things are still sane enough that the viewport tag will eventually become part of CSS, not HTML [1].) And pelase don't suggest Safari's Reader View as an alternative: it will happily skip tables and short paragraphs, without any warning. Moreover, if it didn't do these things, why not make that Reader View the Deafault View for CSS-less HTML documents? Arrrgh!

[1] https://www.w3.org/TR/css-device-adapt-1/#viewport-meta
> QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each.

And formal proofs don't make your confidence higher? IME they're the most efficient tool in the toolbox if you need to get to really low defect rates. (Of course, the sad economic reality is that for most consumer software even a 5% defect rate is perfectly acceptable).
> but not good enough if you're working on Apple software

Why not?
I'm not familiar with the wider thesis you seem to be advocating, (could we get a link?) but calling porn a "cult" seems like a stretch, it's not something that has been created by a group and spread through brainwashing, porn is throughout history and across cultures.
So imagine an ICO company that has a premine. You know the address of all their funds that they raised, and you know all the funds that are held through their premine. You can easily track the money to make sure nothing fishy is going on. This isn't that big of a deal for a tiny company, but imagine this for a huge corporation or government body.

All of them CAN produce auditable records for the consumer, but they don't, blockchains force the issue.
"High-end web tooling is almost exclusively JVM based (Kafka, Cassandra, Elastic Search, Kibana etc). "

This is what's making me want to move away from .NET. Most really interesting development is done in Java and Linux. With .NET and Windows you are often a step behind.
.NET core is lacking so many features it's ridiculous, we've had to downgrade 2 projects recently because even MS Azure service APIs weren't supported - if you have to work with .NET avoid core and save your self the hassle - it's still alpha quality in many aspects after years since "1.0". I regret pursuing .NET career at this point, all recent developments on the platform are a joke - despite the praise they get for OSS moves. I'm moving towards frontend these days just to get away from this mess (ironic considering how messy frontend is - should tell you enough about state of .NET core/xamarin)
That account is brand new, so it seems like a shill account spamming for that website
The pornography was extreme. It was found a few weeks before laws were introduced that made it unlawful. This claim has been made many times, in print, and Green has denied it but not used UK defamation law to prevent the claims being made or to force corrections to be printed.
Sorry, I didn't really understand a word of that.
It's a great effort but such development is too slow and resource limited to really challenge commercial solutions. They don't get to make their own ASICs (e.g. Canon DIGIC) so they need to use limited and expensive FPGAs; they can't make their own sensors (e.g. RED Dragon) so they need to use CMV12000 which is a sensor for scientific and industrial applications - fast, but not optimized for image quality (from my limited knowledge! I could be wrong). Most likely they won't get access to latest and greatest OEM sensors like Sony BSIs.

By the time it's out, you could buy either a fully integrated solution that's far ahead technically - from the likes of RED, Canon, Blackmagic etc - or if you're after some exotic application you could just use an industrial camera from IDS or Ximea.

Yes the customization and the abilities around this camera could be endless, but it'd take something really special on that end to overcome to hardware limitations coming from the development model and to make it a viable professional tool.
In addition: by testing a devcard you also, of course, are implicitly exercising the underlying code.

So instead of writing a test for code X, you can test a devcard using X instead, and kill two birds with one stone.

Especially true if you're doing integration-testing, Selenium-style.
Hawaii startup recognized by NASA for life-saving medical breakthrough
There is one : http://www.jasnh.com/
I am aware of the policy. I didn’t accuse you, I said your comment, and the volume of comments like it made it difficult for me to assume good faith. Which is true. I had to rewrite my comment to leave open the possibility you were being earnest.

I can list horrible things the US has done abroad... regime change in Central America, torture and destruction in Vietnam, thousands of drone killings up to the present day. The U.S. has done things at least as horrible as Tiananmen at home and abroad.

These things are openly discussed in this country every day. They are openly discussed on HN. I resent your accusation that I am ignoring them.

To expand my comment on history: due to the massive amount of data and metadata and metemetata being recorded, there is a class of open evil which will inevitably enter the public record. Maybe not this decade, maybe not next decade, but the information wants to be free. For a certain class of events which are both evil enough and open enough, they will be inevitably exposed.
Entire industries can be built on regulatory loopholes, Uber and Lyft come to mind.

Cryptocurrencies are forcing govts to reexamine regulations that I argue are generally favorable to massive institutions/ high net worth individuals and unfavorable to the small timers
You are not the only one.

If all the bugs you find in the part of a program that was not verified, that demonstrates the power of formal verification.
The article alludes to it, but I think that English sentences have undergone a fairly major shift since, say, the mid-1800s or so. Maybe even the early 1900s.

I read a lot of older books, and sentences like that aren't uncommon. There's all kinds of strange word orders, clauses piled on clauses piled on clauses, etc. It takes some getting used to, but after a while it quits bothering you. If you made me speculate, I'd guess the Latin education of most English writers had something to do with it.

Nowadays, it's actually quite striking how short and simple most of our sentences are.
It's definitely not dead.

.NET runs everything from desktop apps to web infrastructure to mobile games - it's a lot more encompassing than building some websites. It also integrates into a vast ecosystem with Office, SQL Server, Active Directory and is backed up by the fast-growing Azure Cloud. Most small, medium and 100% of the Fortune 500 run on .NET code and services.

HTTP/2 is just not part of Kestrel yet, which is the default new .NET Core web server. You can always use other libraries and this doesn't affect GRPC at all (which can easily generate the server from .proto stubs).

And how are the front-end wars over? Asp.net has great integration with all these modern JS frameworks, along with MVC and WebForms which are both still viable and used often. Why does there need to be a "niche" when .NET already does far more?

It seems like you found 1 missing feature and are proclaiming it a failure when the reality is that it's one of the most common frameworks today, and now also runs great on Linux. It'll be around for decades.