throwawayjava

Not because college is wonderful, but more because you cant get unsecured loans to sit at home and read.

(Also, pet peeve: these conversations often compare highly motivated and indepenhdent people who take the no college route to slackers who attend college.

I never see anyone pointing out the fact that highly motivated and independent people who do opt for college often do much better than they could've without the degree. Often in tippy top status/comp finance, medicine, and tech poaitions.

College doesn't make sense for everyone, but IMO it paradoxically makes the most sense for people who don't need it to enter technical fields like SWE. Because those are the ones who will end up on fast tracks after graduating that would be difficult to get on without the degree)

- Dump of CVEs for "Web App X" or "Server X", even though literally zero of them apply to the version that I'm currently running.

- Dumps of port scans with warnings like "Running SSH on port 22 is not recommended" and "Server accepts HTTP. Always use HTTPS".

I assume there are tools that generate these reports because the reports use decent English but the accompanying emails are written in very broken English.

But in practice, I do often find myself browsing my own code on GitHub for a variety of reasons:

- I'm in their office at their machine, but didn't bring my laptop.

- I'm traveling and want to talk about something with someone (I travel with a separate laptop).

- I'm half way through a big refactor and want to go back and see what master looks like. I know how to do this without GH/GL, but the simplest way to do that is to just pull up GH.

In all of these cases, and others, it's far easier to just pull up the file on github than it is to clone the repo locally.

So, given that we do sometimes want to browse our code remotely, the author then provides the (rather niche) criteria that make this a better solution than GH/GL:

"By serving a repo behind an FTP interface, we get these benefits:

- Web browser supported but not required

- Minimized network traffic, sending just the file data itself

- Supported on all platforms, with dozens of clients already written

- Support for both the command line and GUI"

Agree with you that this is a fairly niche set of criteria, but I could at least imagine myself in an environment where this could be a useful tool.

I run mine as a charity now. Its less than 200 dollars a year. The ads just aren't even worth keeping up. Before and during college, when I couldn't afford the 200, I solicited donations from former users who had used the site as a teen but since grew out of it. That worked really well.

Good luck.

But this is true for literally everyone in the company, including the owner. It's a rare business that couldn't change ownership and still thrive under the right circumstances. In fact, there's a whole day of the week that has a nickname because people do this so often ("M&A Monday")

Your "someone with equivalent skills" condition is equivalent to the "under the right circumstances" condition.

So, I'm not sure I see how this is a response to:

> If the company is utterly reliant on a single person, that person is either an equity owner, or should be, and the owner is taking advantage of them.

> are you saying that they're not true even on average?

Yes, absolutely.

I have personal experience with exactly that kind of poverty, and the chronic physical/mental health problems and financial roadblocks to prove it.

Putting your assumptions about my life aside, you missed the point.

The presumption that people "in the interior" are poor and virtuous and people "on the coasts" are rich and morally bankrupt is profoundly wrong.

The presumption that people who "work with their hands" are poor and people who work in technology are rich is also wrong.

There are people in each quadrant of the "interior"/coast/rich/poor divide. The "rich=coast=no morals=tech" trope is just the opposite side of the ugly "poor='interior'=lazy=uneducated" coin.

I'll also repeat one of my original questions: who in the "interior" actually refers to the "interior" as the "interior"? I literally never heard that language until I moved to a coast.

Weekend (or, anyways, short) vacations to Paris are a thing. On the other hand, they are also super cheap historically speaking (< $600 east cost <-> Paris, stay in a hostel and it's < $800 total). My weekend trip to Europe was $500 cheaper than what a friend from Neosho spent on a pontoon and a rental at TR the same summer! We both got a lifelong dream that summer (me: paris; him: boat & lake house boozefest).

Also, I have back issues from sitting all day and he has back issues from standing all day. He should wear a brace. I should get a standing desk. We are both too dumb/lazy to change and will probably both regret it in 10 years.

So. Rich laborers spend too much on stupid stuff and all humans have health issues. News as 11.

Furthermore, the modality of caring differs, and this causes a blindness to others' generosity. The average rich person in SF who cares about their neighbors is extremely unlikely to exhibit that care via churches, but might take in a homeless LGBT youth and donate 20K+ to various humanitarian/environmental orgs. Similarly, the average rich person in rural GA who cares about their neighbors is extremely unlikely to exhibit that care by voting for progressive policies or by offering to shelter LGBTQ youth, but might donate 20K+ to their church every year.

Those groups are invisible to each other because they each think of "civic engagement" in terms of their own preferred modality, not realizing that there are other ways to help.

(Tangentially, people from the "interior" refer to themselves as "midwesterners", "appalachian", "southerners", "mountain states", or, more commonly, just by their state or even region within their state. I've literally never heard anyone from anywhere outside of Boston/NYC/SF refer to that part of the country as the "interior". Where in the "interior" do people actually refer to themselves as being from the "interior"?!?!)

Working 8 hours a day already leaves enough downtime in my schedule to get bored, but not enough to turn that boredom into something productive. 6 hours would be outright hell.

The problem is, the extra two hours don't really provide me with any compelling new opportunities to contribute! That's barely enough time to get at a school and volunteer and get back to work. Barely enough time to get into the flow of things if I'm volunteer programming. Etc.

But an entire additional day off of work would be great. I could commit to do real things. I could bake so much bread for the church's food shelter. I could build an entire web app using the city's open data to help people avoid tickets. I could spend an entire day in a classroom. Etc.

If you distribute service days evenly and treat them like "just another business function" for businesses, then you could pretty much replace the teaching aspect of higher ed with volunteers. 2-3 people prep+lecture+office hours one day a week, 2-3 people are spending all their service hours helping design curriculum, 2-3 people do a day of grading each week. A <10 person team can teach an entire university course @ 1 day per person per week. Multiply across the whole city, every company. Universal 4 year higher education for "free". And there's still tens of millions of volunteer days per week left over for all the other stuff.

They were being intentionally daft. The person who told him that almost certainly did so with a wink and a nod, and saved your protagonist a lot of pain.

You are describing a scientific conference, or perhaps a grant proposal.

Unlike NSF/NIH/etc., they're not really asking for people who have dedicated their lives to a problem to write up a compelling and realistic plan of attack for a hard tech problem. That can't be done in a few minutes of a video, and certainly can't be done if in that video you also have to write your ideal obituary. What they're looking for, I think?, are charismatic and driven leaders.

When people get used to a comfortable life, a predictable job, and a reputation of succeeding at whatever they do, it gets very hard to leave that behind

I think that there's a sampling bias here; in fact, that bias is even pointed out in the paragraph: > At YC, we’ve often noticed a problem with founders.... I.e., this is an observation about FAANG employees who become YC founders.

But the fact is, very few of those drive/motivated Google/Facebook employees leave and become YC founders. So this observation is an observation about a very small subset of the people who choose to stay at GoogleFacebook.

I know a lot of people at the FAANGs who are there because they are primarily motivated by technical and scientific problems. The FAANGs -- and esp their research divisions -- are exceptionally good places to work for people who get meaning and fulfillment from technical excellence.

>Nope.

Hedge funds and trading firms are some of the top donors to/supporters of the formal methods community. They sponsor conferences, hire tons of formal methods experts, buy products and services from formal methods startups, and develop/use formal methods internally.

So...

Yup.

(I do understand there's a substantive point being made, and I think my reply to the sibling comment by temporal addresses that point. So maybe that's the right place to continue discussion.)

In fact, this is exactly what I was thinking about when writing the last paragraph of my comment.

The how and what questions in robotics/manufacturing ground out in formal methods style mathematical modeling in a way that the sort of questions that dominated the last couple cycles of tech did not (because those tended to be behavioral specifications about humans -- click more ads, book more taxis, click the buy button, etc).

Formal methods didn't capture "engagement" or "click-through rate", but they do capture "safety" and "liveness".

Consider any of the examples you give. At the top level of the design process, we need to derisk things that demand mathematical modeling (battery life, car behavior). How do you go about determining the probability of a car colliding, or tease out the various things that might inform that probability? Not (only) by white boarding with business stakeholders or asking consumers, but (also) by building models of how the system behaves and analyzing those models.

Obviously, formal methods aren't a silver bullet, and yes, software engineers will always spend a lot of time at whiteboards and in meetings.

But when it comes to the future of formal methods, the question is whether the systems we expect to take center stage in the software world look like to sorts of systems where properties like "safety" and "liveness" are a) hard to specify, b) lend themselves to mathematical analysis, and c) are critical to business success.

I think the answer to that question is yes.

Well... depends on the company/team :-)

But I think the instinct is fundamentally reaosnable because even the most abusive interpretations of DO-178C tend to demand a lot more attention to quality than even very well-run software projects in other industries.

> For the most part cars and medical devices and stuff don't use FM because there's pretty much no oversight.

This is starting to change, maybe. The automotive companies have been snapping up verification people (and letting them work on verification).

> But any FM stuff has to go through DO-330 and DO-333, which are just as rigorous and intense as DO-178C. The only stuff that has so far is, unsurprisingly, very expensive and very proprietary.

So, it's been a while, but I seem to remember DO-333 being written in such a way that if Tool X went through the process, and if you could produce a deep embedding of Tool Y's logic into that Tool X, then you could piggy back on tool X's certification by using the Tool X embedding. Which is still a lot of work, but hopefully substantially easier than getting a new tool approved from scratch. Also, I could just be mis-remembering or confusing a dream for reality... its been a while.

The world is changing.

In high-growth-potential areas, I think we're starting to see a shift away from the style of software where "what to build is hard but how to build is easier" and toward application domains/products where exactly the opposite is true.

IoT, next-gen factory automation, robotics, ADAS, automated trading, etc. all have two extremely important things in common:

1. It's really obvious what we want the system to do (minimize energy usage; produce widgets without killing Joe the machinist; go to the store and don't kill anyone; make money; etc.)

Unlike with social apps/online communities/productivity software/games, the "what did the customer want" problem is likely not THE key failure point.

2. It's extremely non-obvious how to map those high-level desires onto software.

These application domains, which I think will drive growth in the software industry during the next cycle, are kind of dual to our current ones (web and mobile apps).

So, at the highest level of abstraction we know what the customer wants. That's not the point where we need the most derisking. Also, the hardest problems -- the ones where derisking efforts will land -- are amenable to mathematical treatment. Because of this shift, mathematical modeling tools are going to play a big role in the industries that (I think) will drive growth in the coming decades. And that means the zeitgeist of software engineering will change.

I'm not sure if those mathematical modeling tools will look anything like today's theorem provers and model checkers. Probably only in the same way that Python looks like FORTRAN.

Your second paragraph kind of walks back on this, but I think it's still worth linking to this essay:

https://www.hillelwayne.com/post/uncle-bob/

In particular: ...[he's] welcome to keep shouting that tools won’t help, better languages won’t help, better process won’t help, the only thing that’ll help is lots and lots of unit tests. Meanwhile, we’ll continue to struggle with our bugs, curse our model checkers, and make software engineering just a little bit better. We don’t believe in silver bullets.

Again, your second paragraph already kind of agrees with this point, but the brilliant rhetoric in the essay is actually true: "no silver bullets" is a reason for, not against, the use of formal methods (and any other quality assurance mechanism we can get!)

> adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount.

It really depends. Especially in the case of formal methods for specification (as opposed to implementation formal methods), formal methods can save substantial amounts of time and manpower. And there are already a lot of success stories, and not just in safety-critical industries.

Trucks are great because the extra degree of freedom is a PITA, but unless you're towing serious loads they are mostly just the country version of a lexus or BMW.

I'm not really sure what "low-dimensional intuition" means, but I pretty regularly build models that do not "assume nonlinear relationships between all parameters".

The author explains: however there is one cluster that was built significantly larger than the others and hosted around 2,000 development environment workloads. (This was an artifact of the early days of running “smaller clusters, more of them”, when we were trying to figure out the right size of “smaller”.)

In software, for known behavioral specs, you don't have a real justification until you write a formal proof. Just because formal proofs are uneconomical doesn't mean there's some fundamental philosophical barrier preventing you from verifying your UI code. Doing so is not just possible, there are even tools for doing it.

So really, this is not a Gettier case, because in formal systems a true justification is possible to construct in the form of a mathematical proof.

An example of a Gettier case in a software system would be formally verifying something with respect to a model/spec that is a Gettierian correct-but-incorrect model of the actual system.

There are almost no software systems where we have true JTB (proofs), so there are almost none where Gettier cases really apply.

Uncertainty in software is more about the economics of QA than it is about epistemology or Gettier style problems, and that will remain true until we start writing proofs about all our code, which will probably never happen.

Also, it's not as if rationality is "above the fray", so to speak. Differing relationships to rationality are at the core of major differences between schools of thought in both international relations and economics, for instance.