skysight-inc/HackerNews huggingface dataset:
> Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free.

People seem to always bring this up but what's better? Verified code is about as close as you're ever going to get to bug free.

If you're doing a large proof, getting the specification wrong and not eventually noticing while working on the proof isn't common. You'll likely have something that isn't provable and get proof goals that don't make any sense. I don't think it's a common problem for mathematicians either that they end up proving the wrong thing.

I haven't heard of any examples of complex verified programs where later someone found a huge flaw in the specification. It would be like writing a set of unit tests and a complex program that passed them which had behaviour that goes against what you wanted.
> A lot of liberals are now arguing for a more aggressive foreign policy...

Would you please provide your evidence for this? Or do you mean a lot of Democrats are arguing for a more aggressive foreign policy?
Sure, but you'll get fired anyway with no legal recourse. At least in most of the US.
Ah yes, apologies, I have edited my post to clarify my mistake.
Hear, hear!, from the perspective of someone who's worked on an HPC
resource manager, and fondly remembers data collection/analysis on
real-time micro-kernel-ish distributed systems in the '80s. I don't
want proprietary software, of course; we could hack those '80s systems
in interesting ways, even if it wasn't actually free software.

I've sighed while removing code for systems like Irix, and Super-UX
(which I thought was dead, but seems not to be). Their extended Unix
resource management features were specifically useful for HPC-ish
batch systems. The deficiencies of Linux are partially mitigated if
you restrict the system to one job per node at the likely cost of
wasted cores, but then -- like Bluegene -- you can ask what the kernel
is there for. An example of the issues is lack of a sane way to
manage and account memory for a job's process groups; please don't say
that the cgroups mess provides that. No, OOM isn't what's wanted when
you hit a cgroup limit, for instance.

Then we have no real solution for security in GNU/Linux HPC systems --
or other mainstream systems (even if they did have HPC hardware
support).

Bluegene was interesting, but is now dead.
Maybe it would be more helpful to stop trying to categorize people based on single posts?
In my line of work - subsea handling equipment - the going phrase when things go really, really bad appears to be "EEE - Entropy-Enhancing Event"

Looks much better in the post mortem reports than the equivalent "Sh-t just blew up on us!!!"
Honest question: should economics be interesting? It seems like that should be one of the simplest, most mundane aspects of society.

Enjoyment from successfully navigating complex constraint sets is natural, but turning the mechanisms by which human beings get fed and clothed into a game like that feels less productive than many alternatives.
I don't see a clear mapping of fear to either side in particular, more that they fear different things. For instance, a liberal might be more fearful of guns, while a conservative might be more fearful of foreigners. A liberal might be more fearful of economic hardship, while a conservative might be more fearful of crime.

These are just generalizations, of course.
Can American soldiers imagine that they are completely safe from all physical threats?
"Beware of bugs in the above code; I have only proved it correct, not tried it. " - Don Knuth
Agreed. See my comment next to yours also. The minority party appoints 2/5 of the FCC so Obama was just appointing Mitch McConnell’s pick (but being Obama he gets all the blame for it!)
> so why can't we have a programming language that gives you a full blown logic system

Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way.

There are a few challenges that come to mind with making a practical programming language that can also do arbitrary math:

a) For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose programming language.

b) The languages which attempt to be useful for theorem proving are generally pure functional languages (due to the strong correspondence between functional programming and logic). Most programmers don't like working in pure functional languages, although the success of Haskell shows that there are certainly programmers who do (myself included).

c) The more expressive a type system is, the more difficult type inference becomes. Yet, paradoxically, I find myself writing more types in languages like C++ and Java than I do in equivalent Coq programs. I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice.

Idris is an attempt to make a practical programming language with the full power of dependent types. So it's probably the closest real language to what you're describing.

Z3 and other SAT/SMT solvers take a different approach: they try to search for proofs automatically, and for certain kinds of math they are very successful. But these are generally only for first-order theories or other restricted kinds of propositions, and not great for general theorem proving. They are good for things like proving array accesses are within bounds, or that you never try to pop from an empty stack (at least that's my understanding of their capabilities).
Various difficulties arise in how to have the expressive power play well with type inference

[0]: http://smallcultfollowing.com/babysteps/blog/2016/11/04/asso...
Boring yet still very volatile.

I wonder if or when Rails will settle down and stop changing everything between major releases causing all documentation to be out of date, gems to break, developer habits to break, etc. Not to mention all of the related tooling like Bundler which seems to spit out new and uninteresting warnings and errors every time I update it.

It would be great to be able to write an application using a framework and not have to constantly change the application just to get long-term updates to the framework like bug fixes, security patches, compatibility with new versions of Ruby, etc.

Basically Rails-LTS but not from a 3rd-party (and embraced by the ecosystem).
come on. read between the lines. i'm saying that blocking websites is fascist behavior, not noble work. don't abuse your family's trust by imposing political censorship on them.
If "the lobbyist" had the power over both parties that you are imagining, then net neutrality would have not passed in the first place.

Or do you think that was part of some long game to hide the influence of "the lobbyist" by appearing to lose on that issue, even though that meant "the lobbyist" had to put up with net neutrality for many years (it would have been at least 14 years if Clinton had one)?

Do you explain the numerous other things besides net neutrality for which Democrats and Republicans have consistently been on opposite sides for a very long time as just fake outs by "the lobbyist"?
You'd think that a technology-oriented magazine like wired would at least try to aim for cross-browser compatibility in their infrastructure. But why bother, make your CMS Chrome-only a policy and free yourself of extra testing.

And it's not only wired. I've come across a lot of internal sites and intranets that are poorly tested on anything but Chrome. I know, it's not exactly the same thing as the old IE/ActiveX but it still grinds my gears when it happens.
This is bullshit.
https://blog.mozilla.org/blog/2017/08/08/mozilla-information...
I'm a pretty heavy user of Chrome profiles .. definitely doesn't feel as well thought out in Firefox.
Anyone have thoughts on the opt-out telemetry default?

I had to read the privacy notice they open on start to find out that telemetry was enabled by default.
That's the very premise behind democracy:

That different parties have different concerns and foucses, such that the process of mediating between their different plans leaves us better informed and prepared than listening to a single group.

The problem is that over the last 100 years, psychology has been weaponized and deployed at scale against the public, essentially drugging them on fear and anger hormones until they're incapable of rational responses.

The various factions have entered what can only be described as psychological trench warfare -- locked into positions, toxic things sprayed virtually indiscriminately, absolutely no actual progress.

No one is quite sure what to do to fix this.
I worked with Adam one summer before he had that coq textbook, he’s definitely a wizard of proof automation in coq. I only much more recently learned how ltac case expressions also backtrack!
Similar to the story method of memorization mentioned, using the Method of Loci makes it easy to memorize all twenty.

https://en.wikipedia.org/wiki/Method_of_loci

https://www.ted.com/talks/joshua_foer_feats_of_memory_anyone...
The customer paid the ISP for bandwidth and Netflix pays AWS for outbound bandwidth. Both parties are paying providers for the requested capacity. ISPs in other countries can provide service at lower prices that US ISPs so I find it hard to believe this is a cost of service argument. The truth is that cable TV is being displaced by network delivered video and the ISPs know they can’t easily replace the cable revenue b6 jacking up internet access fees. Repealing net neutrality provides cover to shift revenue from cable to internet.
I will disagree.

As a newbie hardware designer I learned a lot going through some of those resources. Especially repair videos tend to show a lot of tricks I would have to spend a lifetime to learn by myself. Once you learn the basics (it is easy) it gets more and more difficult to find really usefull information. Especially if you are a hobbyist and don't do it as your permanent job where you would typically have other nad hopefully more experienced engineers at hand.
A minimalist guide to tmux
Fake news sites (real fake news, not how Trump uses it) are malware for the mind. These are things that are 100% fictional and made up to deceive readers for clicks.
Because, in a "normal" case of a large suspension bridge failing, you might kill 20-30, if a bus was going over as it failed. Fixing it might cost $Bs.

In the case of a nuclear meltdown (or "temporary fission surplus") you might acutely impact 10-100s of million people and significantly shorten the lives of several 10s of thousand (see Chernobyl). Costs might range into the many $100Bs.
I've seen enough break in user space in an HPC context. Note that HPC communication needs to happen there.
If you're a programmer that's not tried theorem proving before, I highly recommend giving it a go. It gave me the same 'thrill' I got when I first started programming as a 14-year old and realised a new way of thinking. I find it sharpens your mind in a new, and different way - that's really an exciting feeling.

I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Coq however, is probably easier for most programmers to experiment with.
Nope, he just got 3 million votes less - but the way the voting system works is that absolute number of votes doesn't count, how they're distributed in states count.

The current President didn't design this system, and the opponent could just as well have benefited by it (and previous presidents had).

Lacking direct democracy, it's not even necessarily a bad system in itself (whatever one believes for the current president). It might even be more representative of the average American than the popular vote (if e.g. the majority of the 3 million votes are concentrated in a particular state or two. IIRC the President got something like 50 million votes?

Imagine an exaggerated (but possible) case where 3 states push 50 million votes for one side, and the 49 rest of them push 47 million votes for the other side between them. Would you say that would be a good result, to have a president that has a majority that is based on 3 out of 52 states?

It might not have been as bad in the elections, but a huge part of those 3 million votes where mostly from one state, not distributed more or less evenly across the country. Which is the kind of issue the idea behind the election system wanted to avoid.
> "real fake news"

https://en.wikipedia.org/wiki/Slippery_slope

or (to play coy): you're suggesting we block fiction from the internet...?
It isn't for everyone, but I host my own NextCloud instance on a personal server. Works fine after a bit of tweaking, but it can be a pain to set up.
Thanks, although link doesn’t support anything in parent commenter’s claim.
I fear the actual migration, not the alternatives
The actual quote is: "Internet providers must not manage their system in an anti-competitive way that limits consumers’ choices"

Does not sound like opposition to the repeal.

Of course ISPs are going to claim this fosters choice and competition.
Similar observation has been made in the Wall Street.

When people get their "Fuck you money" (subjectively enough money that they feel safe and can keep their lifestyle and status) they turn more liberal.
I would help organize a NYC meetup;
let's coordinate via email or the like?
Is that partially a tooling problem, i.e. would it help or even be possible to show those intermediate “proof states” (as used by the grandparent) live in the IDE while you type?
Cable TV is dying and you’re correct that this is an attempt to secure higher rent for the internet service that is displacing cable
At the Ice Age Salad Bar
I wish they had some better UX designers. Hit the download button and I get a .bz2 file with no install scripts whatsoever.

$ tar jxvf firefox-57.0.tar.bz2
$ cd firefox
$ mkdir /usr/local/firefox
mkdir: cannot create directory '/usr/local/firefox': Permission denied
$ sudo su
Password:
# mkdir /usr/local/firefox
# cp -rv * /usr/local/firefox/
...
# ln -s /usr/local/firefox/firefox /usr/bin/firefox
ln: failed to create symbolic link '/usr/bin/firefox': File exists
# mv /usr/bin/firefox /usr/bin/firefox.bac
# ln -s /usr/local/firefox/firefox /usr/bin/firefox

Why couldn't they go the extra mile and give me a .deb file I can just click and install or dpkg -i, like Chrome does? Make it absolutely frictionless -- lubricate the whole process -- if you want people to use it instead of Chrome.
I used to be very interested in Software Architecture, in fact I've read many of the papers cited here.

When I did a startup many years ago, I committed the mistake of paying too much attention to the architecture of the software [1] I was writing, and not enough attention to the product/customer side of it.

The last couple of years I've been de-emphasizing software architecture as an interest, and have been paying much more attention to how product teams build successful products, what the patterns are, etc. I was lucky enough to work at Facebook for a while and got to see (and learn) a very successful working model of product development.

So, while I'm not saying that software architecture is not important (it is), also pay attention to the product/customer side: what choices (software, organizational, hiring, business) allow you to move fast and iterate, to release early and often, to run A/B tests, etc.

I think good software engineers are just as much product guys (and data guys) as they are software guys.

-

[1] https://github.com/scalien/scaliendb
Nor is giving away money necessarily an unalloyed good; it can create dependency.
As a very crude example, imagine if there were "invisible walls" in our universe like many video games have. Were we to bump into one, or somehow find it, we would then try to figure out a scientific explanation, but if we ended up with a bizarre, labyrinthine theory after trying our hardest, well just maybe we are in a simulation. You could then try to come up with how our simulation works, and then come up with tests to prove those theories.

Now, in the end, if we are in a simulation, that simulation (or one of its "parents") is reality, and so effectively we are all bound by the physics of the base reality, so one could argue that there is no harsh line between our simulations' physics and reality's physics, but that's another thread ;)
Digging up my school geography from memory I think it means Central Business Distrct?
My gut reaction was to be suspicious of Mozilla, but then I remembered that they're Mozilla. They're probably just trying to figure out which features are confusing for users.

It's strange because we do this type of tracking in all facets of webapps, but desktop apps trigger our suspicion meter.
Try ASP.NET. It’s managed to take learn most of the lessons (what to avoid and what to replicate) from RoR and is built around a better language (C# or others of your choice) and environment (Visual Studio and MSDN) to boot.

Now that .NET with .NET Core is officially a first-class citizen on Linux, there really no good reason not to embrace it.
And yet 95% of the time I try to watch YouTube in Firefox, it just hangs, never actually playing. Yet Chrome works flawlessly every time.

I'm not saying Google is doing anything malicious here, I think it's more of a "we put a lot more effort into making YouTube work" kinda thing.
The speed increase in Firefox has been something I haven't seen in a browser update for years.
I wish there was a way to import passwords in to Firefox Quantum.
I'm not sure why you were DV'd, but in grad school in the US a C is considered failing.
Coding bootcamp in or around India
I am trying to find a good coding bootcamp in or around India. I have done some basic Oracle training and have done a 2 month course on Redhat Certified System Administration (everything except networking).

My criteria for a 'good coding bootcamp':

(1) Should be physical classroom (not virtual).
(2) Focus on full-stack with back end preference for Python or Java
(3) Provide some placement assistance (not as important as first 2)
(4) Closer to Delhi, India the better. Bangalore, Hyderabad, Chennai etc are still good. If there is something great available in Singapore, Hong Kong, or the UK (have some family near London that can help me save on food and lodging) I am willing to spend a little extra.

Any help will be greatly appreciated!
The last year for S&P has been tremendous.

I truly wonder in this age of high asset prices, which assets are relatively best. Stocks won the last couple of years but after that
> the amygdala, is actually larger in conservatives

This[1] seems to be the source study on 90 "young adults"

Seems like( not sure if same name or what) this paper is authored by british actor colin firth who seems to have no actual research qualifications on his wikipedia page.

These people clearly have an agenda. Gross!!

1. http://www.cell.com/current-biology/abstract/S0960-9822(11)0....
I simply don't want the technology I use to be the arbiter of information. Teaching people to discern quality sources for themselves is far better IMO.
Without getting too much into politics, I agree with you 100%, unions are the way to go.
What did they do? Force them to read?
sshuttle hasn't had an actual release in 5 years according to the github project.

If you're using a windows client I recommend bitvise tunnelier.
The astonishing thing for me is, that this is not at all new:

https://en.wikipedia.org/wiki/Defeat_device

Yet everybody involved acts totally surprised.

So good, that they do strong punishments, but maybe don't stop with VW, as others apparently do the same now (or working on it to put it silently under the carpet). Which makes me wonder if there is some backdoor agreement, that VW gets the public shame now, but recieves funding/legal aid, etc. from other companies as they are all involved in this and they don't want VW do the aggressive defense, of "everybody else is doing it as well" ...
This is why phone numbers are 7 digits long: xxx-xxxx. Then, add another "chunk" for the area code: (xxx) xxx-xxxx.
Oh, believe me, they know
That's great new unless your party is the one thats generating most of the fake news, A.K.A GOP/Trump.
Speaking for myself, and I tend to make practical choices for what I understand now. At the moment, I am not using Rails in my day to day work, and this is largely based on my past experiences.

Pros:

- easy enough to find libraries for most things I wanna do

- community likes testing, as do I

- community seems to focus on business & web implementations, so good for those use cases

- lots of questions for which I want answers already answered

- package management

- deployment to PaaS/Herorku-ish platforms pretty easy for smaller teams

- here in San Francisco, there are lots of job opportunities for Rails developers

- I like Ruby, even though I am less excited about OOP these days

Cons:

- Rails is magical & opinionated, and that always annoys me

- Figuring out where some method is coming from in a Rails object is often a pain

- In Elixir I almost never need a debugger, but in Ruby I almost always do

- loading Rails apps can get really slow, and learning to wait for software to boot isn't a skill I like to develop

- I feel more pressure "to do it" right when the time "to do it right" simply doesn't exist for reasons, because trying to come back and refactor gnarly Ruby code is just harder than it is in a compiled language

- Ruby has to be installed on the system to which an app is deployed, and needing to think about how to pre-install Ruby or how long a Ruby install takes is a mild pain (stand alone Go binaries or Elixir releases are pretty sweet)
I don't think people understand that boring tech is where most of the jobs are
Unfortunately, smart tactics make proofs even harder to read. :-)
It is an argument that goes along with it. The refrain (and argument given by parent) about NN is that you can use your voice as a consumer to go elsewhere (to another competitor) in a non-NN world if they are dissatisfied with their ISP's NN policies. The problem I outlined shows that isn't really an option for many Americans.
I think part of the point of the parable is that speed does not matter as there is no 'goal'. We all are just wandering about aimlessly enjoying the wind and sunshine. Sure, some move faster, but just to the other side of the big lake to have to scoot around. Some don't move at all and work on their tans. If you like the wind in your hair, find/make a fast boat.

(I think the parable starts to break down though. How to describe nations, laws, gender issues, etc? It's too much for such a 'happy' story to go into any depth.)
I would tend to agree with this. Many top managers want people who will do dirty work for them if told to, especially in the usual case where they themselves are at little risk from prosecution themselves. Particularly in certain fields like finance, a strong sense of morality or ethics would be perceived as a serious liability.
Could you please not post unsubstantive comments to HN? We're trying for a higher standard here.

If you'd take a look at https://news.ycombinator.com/newsguidelines.html and https://news.ycombinator.com/newswelcome.html and follow the spirit of the site, we'd appreciate it.
> hoping he would destroy a free and open Internet

Many of us disagree with the equivalence between nn and "free and open internet".
What would you suggest if you don't know rails?
Why not use your package manager?
Never; who needs that kind of distraction, especially from some random website you happened to visit?