Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Programmers who want to change how we code before catastrophe strikes

theatlantic.com

Post reply on HN
Print view View original

251–260 of 274 posts

Re: Programmers who want to change how we code before catastrophe strikes

#251

Post by ellius »

michaelchisari wrote: post #164
fusiongyro wrote: post #119

Earlier quoted context omitted.

I feel like this is part of why Brooks says build the first one to throw away, because you're going to. People seem quite unable to imagine life with a program that doesn't exist. Building a more precise specification would be valuable if people were really able to evaluate the specification as if it were a program, but they don't seem to be able to do that. So we wind up building the whole thing to see if it's right…

> Brooks says build the first one to throw away A great theory, but all too often, companies have a hard time scheduling time for a rewrite, and the hacked-together rough-prototype code gets pushed into production in perpetuity.

I code for a couple of the other groups in my division as a favor. I still run our entire QA group out of a folder called "mock database" for this exact reason.

Re: Programmers who want to change how we code before catastrophe strikes

#252

Post by scroot »

bitwize wrote: post #206
igravious wrote: post #97

So. Minus all the doom and gloom. Better safety harnesses, better developer abstractions, more interactive/responsive programming environments. Whatever Bret Victor's selling, I'm not buying. He's the type of self-promoter who doesn't acknowledge all the actual hard work that has been going on for decades in all of these areas.

Bret Victor is like an "all-mouth-and-no-trousers" version of Alan Kay. And many of his talks recapitulate work that Kay and Ingalls did in Smalltalk and Squeak in their various forms. His sexy presentations very closely resemble the "Active Essays" that got promulgated in the Squeak project in the 90s.

Dude's got a research lab where they're building things. What counts as trousers?

Re: Programmers who want to change how we code before catastrophe strikes

#253

Post by tetha »

jbattle wrote: post #109
haskellandchill wrote: post #59

Earlier quoted context omitted.

No, we need to use logic and set theory and provide tools for visualizing the implications of our rules and checking correctness of desired properties. There's a strong history and lots of good people working on these things but it's tough to get our message out to working programmers. This article helps but based on the comments we've got a lot of perception work to do :)

Yet! The 911 outage described in the article was the result of crossing a threshold that was - logically - dead simple both in how it worked and how it was to be understood. The issue was that normal operation of the system pushed through that threshold. The problem here wasn't that the software was changed in a way that made it perform unexpectedly. I don't have a silver bullet, or at least not a pithy one. But I do…

In my book, operating software is a different skill set from writing software.

In the 911 outage, my first thought was: Alright, we have a server accepting calls, and dispatching calls. If there is too much of a difference between incoming and dispatched calls, there is a problem. Maybe it's a capacity problem and we don't have enough 911 operators, maybe it's a software problem, maybe we're dealing with a DoS. I don't need to know or understand anything about the dispatch software, and I'm pretty sure I can monitor, measure and alert these metrics independently from the software.

We can twist, turn, push and shuffle Dev, Ops and DevOps around, but good operators largely try to mitigate failure and risk, including their own limited imagination how much infrastructure and software could fail at once. That's a very different skill than trying to make a single component in a network bug-free.

Re: Programmers who want to change how we code before catastrophe strikes

#254

Post by hwayne »

combatentropy wrote: post #211
hwayne wrote: post #93

Earlier quoted context omitted.

Sure! I've written a quick demo here[1] and a longer-form piece here[2]: [1] https://www.hillelwayne.com/post/modeling-deployments/ [2] https://medium.com/espark-engineering-blog/formal-methods-in...

Is TLA+ pseudocode? It doesn't actually do anything, right? Your example with updating servers, it will never actually update the servers, right? After you try it out in TLA+, you still have to write the real code in some other language, like Bash. If so, then isn't there still a risk of bugs in your Bash program, from typos, leaving out something from the TLA+ plan, or otherwise miscopying it? If so, TLA+ does less…

Yeah, TLA+ just verifies the spec, not the actual code. You still need to write tests and use code review and the like.

Re: Programmers who want to change how we code before catastrophe strikes

#255

Post by hwayne »

kmicklas wrote: post #245
AnimalMuppet wrote: post #80

Earlier quoted context omitted.

Type theory is much less than "correct by construction" formal methods. Type theory is great at preventing a whole class of bugs (an operation on a value for which that operation doesn't make sense). But it's inadequate for the larger problem, of whether the operation is the correct one. Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the fo…

> But it's inadequate for the larger problem, of whether the operation is the correct one. Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.

What are some good examples of complex system properties you've seen verified with sufficiently advanced types?

Re: Programmers who want to change how we code before catastrophe strikes

#256

Post by rurban »

justherefortart wrote: post #60
david927 wrote: post #30

Earlier quoted context omitted.

What went wrong with Visual Basic? The language was simple enough for beginners but not sophisticated enough to scale for large projects. All too often you would have a project that started in VB as a proof of concept which then extended to become the actual system, and then as that system grew it started to collapse under its own weight. The conversion to the CLR fixed a lot of that, but now it isn't really for begi…

Visual Basic was fantastic for kicking out a UI. If you needed anything larger, all you had to do was build DLLs and reference them. So easy front end and easy back end. The best of both worlds.

Visual Basic was also fantastic to kick out multithreading server code. The problem was always libraries and lack of language reflection.

Re: Programmers who want to change how we code before catastrophe strikes

#257

Post by kmicklas »

hwayne wrote: post #255
kmicklas wrote: post #245

Earlier quoted context omitted.

> But it's inadequate for the larger problem, of whether the operation is the correct one. Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.

What are some good examples of complex system properties you've seen verified with sufficiently advanced types?

Probably the poster children of verification:

* http://compcert.inria.fr/

* https://sel4.systems/

Re: Programmers who want to change how we code before catastrophe strikes

#258

Post by sjm »

This seems over the top to me. Everything has issues, and everything is increasingly complex, not just programming. Take any industry and over a long enough time-span I'm sure things have also increased in complexity in drastic ways. Sure, programming is relatively new, and we are ramping up fast, but we already have vastly complex systems, tools, and infrastructure relying on programming which has incredibly impressive uptime and efficiency.

Yes, people will die from errors in the code of autonomous cars, but at the same time can anyone argue that autonomous cars won't be significantly safer than us?

The argument here seems to be that it's dangerous if the programmers relying on StackOverflow to copy/paste solutions work on real problems without "stepping up". I think that's like someone suggesting a bricklayer would suddenly be in charge of designing blueprints for a 150 storey skyscraper. They are different jobs performed by people doing very different things. They may write code in the same language, but they're not in the same profession.

Re: Programmers who want to change how we code before catastrophe strikes

#259

Post by HumanDrivenDev »

arjie wrote: post #230
HumanDrivenDev wrote: post #203

A lot of it comes down to the fact that this isn't engineering, and we aren't engineers.[0] The field has a very low barrier to entry (much lower than a bachelors degree). The standards are low, the expectations are low, and there's a strong anti-intellectualism streak. Don't believe me? try talking about "esoteric" stuff like category theory, logic programming, LISP or writing functional specs. At the workplace most…

We're the last market-driven field. So most companies take the attitude of "Take your approach. I'll see you in the market". This isn't anti-intellectualism or realism or pragmatism. This is a different fitness function for software. Bug-free programs aren't inherently good. If I'm building X-ray scanning software I'm going to be careful. But if I'm writing a Slack lunch bot in Coq for anything but the fun of it, I'm…

I'm not talking about anything as ambitious as making all software be formally verified.

All I want is for the people in this industry to take it seriously, for us to have standards as an industry, and some kind of professional certification to exclude those that don't know the basics. Software is rife with cowboys and it harms the image of those of us who actually care.

Re: Programmers who want to change how we code before catastrophe strikes

#260

Post by HumanDrivenDev »

Aeolun wrote: post #217
HumanDrivenDev wrote: post #203

A lot of it comes down to the fact that this isn't engineering, and we aren't engineers.[0] The field has a very low barrier to entry (much lower than a bachelors degree). The standards are low, the expectations are low, and there's a strong anti-intellectualism streak. Don't believe me? try talking about "esoteric" stuff like category theory, logic programming, LISP or writing functional specs. At the workplace most…

> category theory, logic programming, LISP or writing functional specs But does it fix my problem? I'm sure category theory is interesting for it's own sake, but it won't help my boss add this extra attribute to our product, so it won't help me get paid. Given that I've already added fifteen form fields this week, my mind is too overburdened to care much about category theory, which will have exactly zero relevance t…

If your role in a company is so removed from the business or stakeholders that you're being assigned tasks like "add 15 fields", then IMO you're already in trouble.

That's part of a larger issue though, where we actually let non-technical people dictate technical specs to us.

Post reply on HN