skysight-inc/HackerNews huggingface dataset:
> One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their[sic] is a corresponding equivalence of the two activities.

Don't take this as an endorsement of proof assistants, but programming and proving are special cases of a single general activity: constructing a mathematical object.

> Both physicists and mathematicians solve equations, but no one would say that physics is math.

The crucial difference is that physicists, unlike mathematicians or programmers, don't create universes of their own. Their job is to explain the behavior of the one that already exists.

> Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable

Only because they have made them so. Also, insanely irregular and intractable mathematical objects do exist, yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof.

> while programmers manipulate very irregular and very intractable objects.

Only because they have made them so. Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning.

> The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity

Then quantify the bug, and make it a part of the specification.

> (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable)

Bugs occur in the program, not in its execution traces.
Ask HN: Recommended licenses for free binary distribution
We are considering making our software available for free for non commercial use. We will not distribute the source code, just the executables. I was thinking about using a creative commons license, but in their FAQ they recommend against using their licenses for software. Are there any better options?
If you go talking to police about a crime you're accused of there's a good chance you'll need a lot more help from a lawyer than if you'd said nothing.
1/3 of all people killed by strangers are killed by police officers.

https://granta.com/violence-in-blue/
> It was assumed that hardware would scale to keep up with demand,

No, it was designed to stay at "one block every ten minutes" regardless of the hardware added or overall hashrate of the system. Which is why you hear a lot of people arguing over block size and block compression: you always have one block every ten minutes, how many transactions can we squeeze into that block?

The only thing that adding more hashrate does is waste more power, since the network will adjust.
How many years did it take the professional to play 100,000 games? How many minutes did it take AGZ to play 44M? It sounds like self play is rather fast to me.
In 1965, Peter Landin presented the groundbreaking paper "The Next 700 Programming Languages" at the ACM Programming Languages and Pragmatics Conference in San Dimas.

It described a family of languages called ISWIM, with a staggering number of durable inventions. It's widely recognized as the precursor to ML and Haskell. One of the inventions is the "off-side rule" for indentation sensitive parsing.

The last section of the paper, after the author's conclusion, is a transcript of the discussion at the conference. The first question is from Naur:

Regarding indentation, in many ways I am in sympathy with this, but I believe that if it came about that this notation were used for very wide communication and also publication,you would regret it because of the kind of rearrangement of manuscripts done in printing, for example. You very frequently run into the problem that you have a wide written line and then suddenly you go to the Communications of the ACM and radically, perhaps, you have to compress it. The printer will do this in any way he likes; he is used to having great freedom here and he will foul up your notation.

Next, Floyd:

Another objection that think is quite serious to indentation is that while it works on the micro-scale—that is, one page is all right—when dealing with an extensive program, turning from one page to the next there is no obvious way of indicating how far indentation stretches because there is no printing at all to indicate how far you have indented. I would like you to keep that in mind.

It's a very old discussion.
He just said nodes validate the information. It just doesn't matter to anyone else other than the node operator and users of that node.

The only occassion the propagation is valid if you're transferring a transaction from another full node to a miner (or helping to do so). As long as there is any path to do so more nodes do not matter.

All miners are already connected together using high speed channels.
To be fair, becoming a quarter trillion dollar store of 'digital gold' is a hell of a pivot.
Or more realistically, better sensors.
Ownership (by devs) doesn't have to mean a hyper-personalized idiosyncratic creation. Part of the pride of ownership can be making something understandable and modifiable by other people.

The bigger problem is that many companies do not reward that, they reward doing it quickly and not asking too many questions.
Proprietary hardware can have a hardware backdoors.
How is this expected to work with 7 billion people using it for every tiny financial transaction? I don't think it can.

It's not meant to. It stores wealth. Nothing more.
https://pbs.twimg.com/media/CzfP6dNXAAAB53_.jpg:large

You might call this excessively cynical but it has a point. If a police officer wants to arrest you there isn't much to stop him.
"There was a shooting. Please send police and ambulance" and then hang up?

Won't the police show up expecting an active armed gunman? Is there anything you can say to show that there is no new danger of violence without implicating yourself?
This is the most Hacker News “please rich daddy notice me” thing I’ve read in years.
Yep, a non deflationary currency would be precisely one that has its coins created all the time, instead of in a predefined amount as bitcoins. (You can think of mining as "discovering" one of the predefined bitcoins instead of creating a new one).
The problem is that for a currency to be slightly inflationary, as it should be, you need to tie it to an economy and make political decisions about it- and then you're back at square one.
Coins like NXT already use proof of stake. And NEM has so-called proof of importance.
Do you know how that might play out long term? I'm rather fond of their approach but then I see the top coin holders get almost all the rewards for "forging".
I'll read your linked document in a bit when in not on mobile anymore
AMD already building coin mining optimised gpu's, making the algorithm memory-hard to exempt asic's doesn't really change much except the direction of hardware manufacture
See, here's the difference - I'm talking about a pattern, and you're talking about the exact situation. You can't train most people to act according to each individual situation in an intelligent manner, especially when situation is very scary, and those rare people who can be trained to do this are usually in special ops, not in regular police. So, when considering a police or military response to a situation, consider a typical situation with these data points.

Oh, and I completely forgot the fact that a decision like this should be taken in a VERY short span of time - you can't turn on intelligence for this, it HAS to be trained.

For me, algorithm adds "possible weapon", "suspect understands that we're pointing guns at him" and "arm reaching down" and automatically goes to "open fire" is the only possible one.
Because the whole 2016 roadmap and the whole 2017 roadmap was also about scalability. All they've done so far is throw their hands up and say "it's a really hard problem trust us guys". And nobody has shown any sort of traction on a solution: the developers admitted Lightning Network won't solve scalability concerns.

Some people are getting a little tired of the pony show.
> One view of management is that it's about making sure the cogs of the machine are completely interchangeable.

That's not what I was talking about. Employees are neither bricks nor cogs. But having said that, if you run any long-term project, you should expect people to come and go, it's part of the game. Thinking that this will not happen in your project is simply negligent.

> This is actually an extremely inefficient and demoralizing environment for those involved.

It doesn't have to be. Working with common conventions and tools doesn't have to be demoralizing. Conventions should be set for a good reason, after an open discussion, and possibly even a vote ("Do you think that it's worth bringing in this library?", "Should we all use the same IDE?"). Also, conventions aren't set in stone, they can change over time.

This gives the team ownership of their project. It makes passing knowledge between team members easier, it makes it easy for team members to help each other when they've run into an issue, not to mention that it makes code reviews and various technical discussions a lot easier.

If Bob is writing using a different language or a set of libraries than the rest of us, who can review Bob's code? Who can help him out when he's stuck on some bug? Who can help him flesh out his design ideas for some feature he's writing?

Without team cohesion, you're creating not a team of developers, but a bunch of individuals who happen to work on related stuff. I don't know about you, but to me that sounds a lot more demoralizing. To me, one of the great benefits of working on a team is that we all get to learn from each other, plus we get to share a common goal. Agreeing to some common conventions seems like a small price to pay for that.
> Probably anybody who reaches the level of 1 dan or higher in Go has at least a Mensa-level IQ.

I've never been able to get past 4k. But from having watched a bunch of Bats go lectures on YouTube, he says (and proves) that it's possible to get well past 1d on direction of play alone without having any problem solving ability.

https://www.youtube.com/user/dwyrin/playlists
Achieving excellence has a personal cost. Imagine that.

The other thing is that the first test that gave rise to the concept of IQ tests was not intended to measure intelligence. It was intended to measure school readiness for rural French children who often did not have birth certificates, so age could not be used as an indicator of school readiness. The problem was complicated by the fact that rural kids and city kids had different experiences that left the rural children less equipped to cope with the school environment. City kids were more likely to have already participated in preschool, among other things. So, there was a cultural divide.

The idea that some people are simply innately smarter is something that is very much debatable. IQ tests are highly influenced by deep cultural knowledge that is typically available to cultural "insiders." In the US, this is typically upper class and upper middle whites.

If an American takes a British or Canadian IQ test, they will tend to perform more poorly and show as having a lower IQ than on American tests, even though these are all English speaking countries. The effect gets worse if you are taking it in a second language. But it still exists even if it is merely a different culture, not a different language.
Dropping low-fee unconfirmed transactions is not the same as not accepting transactions.
If you want to make really smart friends go to weird al concerts.
The piece you are missing is that this problem is a direct result of the Core dev teams deliberate choice not to scale. They have a strangle hold on development and vehemently opposed any proposal to scale through block size increases as was the original intent.

Bitcoin Cash isn't having these problems and won't have these problems in the future. Many people aren't aware of the underlying issues driving the transaction backlog in part because the historically important forums where Bitcoin is discussed have suppressed any discussion of this issue for a couple years now.

https://www.yours.org/content/a-roadmap-for-scaling-bitcoin-...
Great execution, I had the same idea a while ago after playing with mitmproxy. My concern would be that people would tentative towards using it as you can tamper with requests on the server which they don't have control of.
I agree. To model any complex system, it only really requires that a person or a group of people understand, and are able to codify their knowledge the system for a given period of time.

Just think of your average decently sized code base. There's enough complexity there such that any single human can't understand it at a given time, save for a very high-level explanation.

Does this mean that we don't understand the code base? I don't know if that's the right way to think about it.
>this is the norm within the industry and is intended to ensure information accuracy

I like how even they understand that it's a bullshit clause, and try to justify it.
Their own young, a fair few species (lions come to mind) kill the young sired by other males.
I'm not a PhD, but I always like to think of this explanation when trying to understand how progress happens. In bumps.

http://matt.might.net/articles/phd-school-in-pictures/
Well, for instance, not everyone has rules where the police need a warrant to search your home or vehicle.
>There's no evolutionary drive towards simplicity.

There's a drive towards smallness (as in, lower food requirements) which has probably made simplicity a lot less bad than otherwise.

>In physics, much is out of reach of experiment due to being either too small (superstrings, if they exist)

In the era of Maxwell's equations, atoms were too small. Never under-estimate the power of cleverness and indirect observation! (Now days we can image atoms directly: but we needed to get our understand of them elsewhere in order for our technology to advance that far.) The jury's still out on strings; although plenty of people claim that we won't ever reach the energy scales necessasary to totally rule it out, we still might find something predicted by a lower-energy version, and maybe one day we'll uncover a new theoretical result that gives us an avenue we can't currently see.

>or too big (where's the missing mass and the antimatter?

That's not too big, we're expecting the answer in the form of slight asymmetries in particle interactions like the ones we're studying in the LHC.
The IRS classifies and taxes it as an asset because functionally it is an asset. The design is speculated to be based off of hashcash and maybe it was suppose to be used as cash and in a way it is still useful as "electronic cash" for online orders since wait times are less relevant.

http://www.hashcash.org/papers/hashcash.pdf
Except Bitcoin is inefficient by design (it’s what proof of work is) and the dosage is the market cap and transaction load. So what you’re really saying is bitcoin at the scale it was meant to operate at is poison.
Sure, so if you use Ada you can write types like this and the runtime will enforce your invariants automatically. What other non-academic languages support that? It’s something I miss from Ada for sure.
How is this better than Charles or Fiddler?
How good you are at Go (or chess for that matter) has no correlation with your IQ. There are plenty of examples of people extremely good at chess that struggle, seriously, with academics (e.g. world champion Jose Raul Capablanca, and the youtuber and grandmaster Eric Hansen). Kasparov doesn't have 180+ IQ, which is a common myth. At some point he took the test and it turned out he had a respectable but definitely sub-Mensa IQ.
It's possible that all iron-based Bronze Age artifacts are made of Meteoric iron
I haven't dealt with those for a while but, as I recall, all the hardware and software companies in the benchmark (which isn't a comparison except insofar as other companies have also published a benchmark) have to agree to publish. Furthermore, the results are audited and there are various rules about how you can use and talk about the benchmark. (And they cost BIG money to run--into the millions $.)
Thanks a lot Malkia, that is super encouraging!

Editing code for game levels seems to me like a quite good use-case for this. "Editing" software with rich hierarchical documents is the itch I originally wanted to scratch with this work, even though there are many other use-cases too. Feel free to send me an email if you move further with that idea or if you want to discuss any of these topics with me :-)
Unfortunately most business people don't make things like "doesn't corrupt the database when an exception is thrown" into a feature bullet.

So while you can argue it's part of the scope, it's not part of the scope that anybody else seems to think about.
The way in which those rights are legally secured (in addition to the rights even conceived of) differs from one country to another, even in countries we'd generally consider as those which respect human rights and the rule of law.
"Because why not":

> While the ideal would be to individually test all participants for IQ we found no scientific data that would give reason to discredit Mensa members in any country from being representative of those with high cognitive ability.

https://ac.els-cdn.com/S0160289616303324/1-s2.0-S01602896163...

I think this entire paper is bogus, it reeks of lazyness. They did not have a control group either, they used general statistics:

> Although the national surveys would likely capture a broad range of intelligence, statistically only 2% of the national data would include those with a gifted cognitive ability such those who qualify for membership in American Mensa, Ltd.

Which is false, 2% of the population does not join mensa.
Keylogger Found in HP Notebook Keyboard Driver
> 'I would like to help you but I have no further comment without speaking to a lawyer first'.

Obstruction of justice? Failing to comply with a LEO instructions? Failing that the dude’s got a gun and he’s not going to be afraid to use it.

I don’t know if you’ve read the article but body cams or no, they will shoot you dead and get away with it.
What is low fee to you? Because there are people paying several bucks to do a transaction right now that are being dropped.
Moving from bitcoin to another crypto currency is still chasing out, unless I misssed your point.
Did anyone else wonder what kind of Lambda job a Horst Faas would be?
How does it work? AFAIK you can't run a local webserver on iOS without a jailbreak.

What's the benefit compared a traditional network setup with a MITM proxy?
I don't claim that Bitcoin is a winner according to the criteria set out by Hayek, in fact it's obviously problematic as a unit of account as you explain.

The various decentralized stablecoin projects (disclaimer: I'm involved with one of them, MakerDAO) attempt to create competitive currency as laid out by Hayek, using collateralization and continual supply/demand tweaks to encourage a stable market price.

From that perspective, Bitcoin is indeed more like a trailblazer and a collectible precious metal, and not a serious contender for actual currency status. Still, it seems to have an important role in the ecosystem of denationalized currency.
Have you seen any announcements from merchants, businesses, exchanges regarding downtime due to congestion? Probably not, because the spam-prevention mechanism built into Bitcoin by Satoshi themselves is working as intended.

On the flipside, you have Ethereum with more or less unbounded block sizes having issues with Cryptokitties congesting the entire network. Numerous entities using Ethereum are unable to do business due to the equivalent of Beanie Babies clogging the network [0][1].

[0] https://www.coindesk.com/ethereums-cryptokitties-blockchain-...

[1] https://twitter.com/myetherwallet/status/874285733707526145
The description of this technique is excellent. I once used this many years ago to determine the hidden depth of card card sharing networks for pay tv. it's not exact but it does help quantify issues with deep unreachable data, and sets a base line to compare against over time.
This is such a silly comment. This is like saying that you have a Bus with 20 seats and 40 people that want to ride. Your advice isn't get a bigger bus it is get to the bus stop earlier. It doesn't matter how early everyone gets there in the end there are only 20 seats.
Maybe it was sarcasm? I hope it was sarcasm, at least, or that the OP is young enough and hasn't had the chance to learn yet.
What Does Hyperinflation Look Like? Take a Look at the Weimar Republic in 1923
datomic is to slow on writes, even slower than sqlite, that's because it serializes all writes.
> programming and proving are special cases of a single general activity: constructing a mathematical object.

Painting your house and painting the Sistine Chapel are also special cases of a single general activity. Or writing a shopping list vs. a novel. That doesn't mean that the motivations, concerns or skills are similar.

> yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof.

Right, they just don't prove much and move on. Again, the motivation is different. In programming the standard isn't even proof. It is bad to spend 10x the cost to ensure zero bugs if the requirements don't call for zero bugs. In the vast majority of formally verified safety-critical software systems, the standard is very high yet proofs are hardly used at all, but rather model-checkers. I am aware of quite a few algorithms proven correct (informally) in prestigious peer-reviewed journal that have later been found incorrect by model-checkers. I am not aware of examples to the converse. Mathematicians don't like model-checking even when completely exhaustive, because their motivation is insight. But for programmers, the motivation is meeting requirements.

> Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning.

And yet, it is uncertain whether this is generally possible, and empirical evidence suggests that real-world instances are close to the intractable worst-case. Wishing for something doesn't make it so -- at least not yet.

BTW, Dijkstra made his more sweeping statements before results about proof complexity were known (initial results in the seventies, and many more in the eighties, nineties and oughts).

> Then quantify the bug, and make it a part of the specification.

It is, just not part of a formal spec. Specifying and verifying probabilistic properties is especially hard and costly, and as someone who has actually used formal methods for real systems in industry, I know that formal methods are not binary. Like everything else in programming, you must weigh the cost and the benefit of every decision.
A lot of people join Mensa not to brag about it. Mensa can be a really good group to join to meet interesting people and make new friends. Lots of members don't discuss their membership outside of Mensa meetups.
Bitcoin is absolutely not a good store of value. A good store of value is a reliable store of value: one where you can place your assets and go back and get them at any later time.

As a deflationary currency, bitcoin would be a hypothetically good store of value if a bitcoin actually had any intrinsic or even just de facto value. But it clearly doesn’t: it’s only the conversion to and from USD (and others) that has given it any value at all as an investment vehicle to some. And _that_ value isn’t guaranteed preserved one bit.
Most of the popular consumer apps use SSL pinning these days.