Programmers who want to change how we code before catastrophe strikes • Hacker News Board

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

#141

Post by ScottBurson » Wed, Sep 27, 2017, 9:12 PM UTC

AnimalMuppet wrote: post #127

haskellandchill wrote: post #100

Earlier quoted context omitted.

8 years of web dev under my belt, but yes I do have some academic pedigree and have been investing my time heavily in the history and techniques of formal methods. I'm hoping to contribute to bridging the gap. Don't get too hung up on set theory, I was just referencing the article.

It is my impression (as an outsider) that web programming might be the hardest environment for formal methods. Yes, I could see formal methods proving that only valid HTML was ever emitted. But how do you prove that your layout aligns on Firefox 55.0.3? So it seems to me that, if you can make progress on formal methods in your environment, you're not picking low-hanging fruit...

> I could see formal methods proving that only valid HTML was ever emitted.

I think we could also prove the absence of XSS vulnerabilities. That would be very valuable.

> But how do you prove that your layout aligns on Firefox 55.0.3?

This is harder, admittely. Mozilla is probably not going to provide the formal model that haskellandchill imagines, unless that model can be automatically extracted from the actual code, which may be possible someday.

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

#142

Post by jauco » Wed, Sep 27, 2017, 9:12 PM UTC

tasuki wrote: post #85

I'm surprised understanding the domain hasn't been mentioned. Whether I am developing for someone else or for myself, it turns out misunderstanding/misrepresenting the domain is the most common source of trouble. If your understanding of the domain isn't thorough, is TLA+ going to be much help?

I think you'll like this article: https://blog.acolyer.org/2016/11/08/on-formalisms-in-specifi...

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

#143

Post by discreteevent » Wed, Sep 27, 2017, 9:12 PM UTC

emodendroket wrote: post #132

valuearb wrote: post #104

"For Lamport, a major reason today’s software is so full of bugs is that programmers jump straight into writing code. “Architects draw detailed plans before a brick is laid or a nail is hammered,” he wrote in an article. “But few programmers write even a rough sketch of what their programs will do before they start coding.” I almost always dive in, but I almost always write my code twice. Essentially the first round…

So basically all our problems will go away if we return to UML and requirements documentation that's hundreds of pages long and edited for ages before anyone writes any code.

No. Have a look at this video. It's worth it. He's just saying that you should think before you code and that most specifications should be just a few sentences stating what you intend to do. Code as a blueprint is not the same.

https://youtu.be/-4Yp3j_jk8Q

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

#144

Post by jcranmer » Wed, Sep 27, 2017, 9:13 PM UTC

Epenthesis wrote: post #35

Jtsummers wrote: post #12

Earlier quoted context omitted.

The analogy would be more appropriate if you said programmer and not software engineer. Anyone calling themselves a software engineer should be providing input into the design of the thing they're producing. Their role is very explicitly managing requirements and codifying them in, well, code. Either directly doing the programming or managing those who do.

Are there companies that actually distinguish between these roles? For all the ones I've ever worked at, "software engineer" and "programmer" are synonyms. (I'm aware that there's been some effort to extend the legal significance of the word "engineer" to the software industry, but I'm curious if that difference is actually in practice anywhere today)

There was definitely a time in the 90's when there was interest in having specialized software engineers/architects produce comprehensive designs for software that code monkeys would be tasked with fulfilling. I wouldn't be surprised if there were places today with strong management bias that thinks of "designing" as high value-add and "coding" as low value-add, and the two tasks as falling under the purview of different individuals.

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

#145

Post by dan_mctree » Wed, Sep 27, 2017, 9:13 PM UTC

ScottBurson wrote: post #92

AnimalMuppet wrote: post #86

Earlier quoted context omitted.

How long have you worked as a professional programmer? Because you sound like a just-out-of-school idealist with an idea of the "right way to do it". That ideal tends to get blunted after a decade or two of experience in the real world. In particular: Set theory ? I don't want to program using set theory for the same reason that I don't want to program using octal - it's the wrong level of abstraction for what we're…

I don't know what kind of code you've been writing, but I've been working in compilers and static analysis for decades, and set theory is exactly the right tool for the job. I don't imagine it's the only thing you would ever need for any kind of programming, but I bet there aren't many kinds of programming to which it is entirely irrelevant.

The quality of the vast majority of my code is evaluated in 'soft' ways. Anywhere from "does this webpages layout work well on all browsers" to "does this AI feel like a challenging opponent" to "did you deliver software results fast enough" to "is the code neat enough and well documented". The part that can be meaningfully tested through any kind of formal system or automation is minuscule and it's very rarely where the problems lie.

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

#146

Post by shalabhc » Wed, Sep 27, 2017, 9:18 PM UTC

vtange wrote: post #49

So we need to write more code to make fancy Photoshop-like editors for the average-Joe programmer who can't see the big picture? That just adds more to the code issue - even Photoshop has bugs you know. The fact that "Few programmers write even a rough sketch of what their programs will do before they start coding" is a soft-skills/experience issue that isn't specific to software. I too can use Photoshop to draw logo…

> So we need to write more code to make fancy Photoshop-like editors for the average-Joe programmer who can't see the big picture?

Rather, the idea is to remove layers of unnecessary mental burden and complexity required, similar to how well designed programming language might reduce cognitive load of dealing with the syntax itself (vs the problem you are trying to solve).

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

#147

Post by shalabhc » Wed, Sep 27, 2017, 9:25 PM UTC

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.

Can you point to what work specifically has improved the situation in terms of `developer abstractions` and `interactive/responsive programming` in the last few decades?

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

#148

Post by ScottBurson » Wed, Sep 27, 2017, 9:48 PM UTC

dan_mctree wrote: post #145

ScottBurson wrote: post #92

Earlier quoted context omitted.

I don't know what kind of code you've been writing, but I've been working in compilers and static analysis for decades, and set theory is exactly the right tool for the job. I don't imagine it's the only thing you would ever need for any kind of programming, but I bet there aren't many kinds of programming to which it is entirely irrelevant.

The quality of the vast majority of my code is evaluated in 'soft' ways. Anywhere from "does this webpages layout work well on all browsers" to "does this AI feel like a challenging opponent" to "did you deliver software results fast enough" to "is the code neat enough and well documented". The part that can be meaningfully tested through any kind of formal system or automation is minuscule and it's very rarely where…

What you're talking about is what I call the "specification-implementation gap". In some domains, that gap is vanishingly small; webpage layout is a good example. Sometimes the specification is as simple as "when the user clicks this button, display this message". There's nothing to be gained by formally verifying that particular property of the specification.

But sometimes the gap is wider. An only slightly more complex example would be "the shopping cart contains all items added to it in the current session and not subsequently removed". Sounds trivial, right? Well, as it happens, just a couple of days ago I bought two items from a site whose cart was broken -- it would show only the most recently added item. (I had to make two transactions. Fortunately no shipping fees were involved.) Okay, that's a rare sort of bug, but it just shows how even very simple invariants can get broken on occasion.

Sometimes the gap is even wider. "This app must have no XSS vulnerabilities." There's no one place in the program where you can see that that property is correctly implemented.

You see where I'm going with this: the wider the specification-implementation gap, the more useful formal methods can be.

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

#149

Post by lomnakkus » Wed, Sep 27, 2017, 9:48 PM UTC

Bartweiss wrote: post #43

chroem- wrote: post #24

The dangerous unreliability of software is an accountability problem, not a technology problem. Engineering disciplines are regulated so that engineers are held personally and even criminally responsible if they endanger property or lives. Software, being the newcomer, has no such regulation. Instead we have people trying to claim that software deserves a free pass from due diligence because "software is hard," when…

> The only difference is that these other engineers are motivated to be significantly more thorough about their jobs. Hang on. Sure, all engineering has hurdles. But how many engineering projects face regular enemy action? The last time somebody actively tried to compromise a system I was building was two weeks ago. How many engineers live like that? We hold civil engineers responsible when bridges collapse unprompte…

The problem with software as opposed to most artifacts that humans produce in the world is: "chaos". Sofware is insanely sensitive to initial conditions and a single logical error anywhere along the line leads to... well, chaos[1]. A single errant system may also have insane reach (as opposed to e.g. a bridge), so the consequenses just amplify.

Unfortunately, we've started to rely on the reliability of software in unprecedented ways. (I'd guesstimate that it's probably mostly short-sighted economics that's driving it.)

[1] This is inherent to Turing Machines[2], so if we keep insisting on Turing Complete languages in every realm of computation we'll forever suffer this problem. Please don't think that I'm making an argument against general computing, I'm not. I'm making an argument for restricted DSLs for things that don't need more.

[2] We're not even talking the 'ordinary' chaos of dynamical systems here. Those can at least usually be approximated numerically for the near future unless they're actually really close to a point of divergence. Not so with programs.

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

#150

Post by vikascoder » Wed, Sep 27, 2017, 9:50 PM UTC

emodendroket wrote: post #132

valuearb wrote: post #104

"For Lamport, a major reason today’s software is so full of bugs is that programmers jump straight into writing code. “Architects draw detailed plans before a brick is laid or a nail is hammered,” he wrote in an article. “But few programmers write even a rough sketch of what their programs will do before they start coding.” I almost always dive in, but I almost always write my code twice. Essentially the first round…

So basically all our problems will go away if we return to UML and requirements documentation that's hundreds of pages long and edited for ages before anyone writes any code.

Thats how most Medical Device software is written :)