Hacker News Reader

Comment by vtange | Hacker News Reader

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 logos, maps, and diagrams, but I'm pretty sure someone out there who uses Photoshop professionally knows a lot more tricks within Photoshop and sees the bigger picture of what they want to create before starting. I generally free-hand my drawings, as opposed to the structured outlining most professional artists do.

View on HN

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 :)

There are definitely people making a real effort here, and I appreciate you. But I can't shake the feeling that the reason your task is so hard is that everyone before you has been selling snake oil. "Visual programming", "human-readable software languages" and so on are all just ways of saying "crippled tools".

It's not an accident that the examples in the article were WYSIWYG editors, Photoshop, Squarespace, and Mario. All of those things flatten neatly into two dimensions, and their terminal form is visual. The visualized code is the product.

Meanwhile similar initiatives for software in general are almost always nonsense. There was a pretty compelling TED talk* about visual tools for cybersecurity, shared by lots of people I know. Only one problem: none of the fancy tools showcased work, or will work. They're operating backwards from a known answer. Like most programming tools, they collapse right where they're needed most, stopping at the same edge cases that cause these problems.

More broadly, it seems like the existing tools for known-safe software run exactly the opposite direction from Bret Victor's vision. Correctness proofs, exhaustive test suites, reversible debuggers, and so on are far from non-code, but they're what we use where reliability matters most.

I can appreciate that "code everything like the space shuttle" is hopeless, and I would love to see breakthroughs on easier correctness checking. But right now, it does feel like an attempt to push tools that won't work when they're needed.

*TEDx, but selected by TED for special featuring: https://www.ted.com/talks/chris_domas_the_1s_and_0s_behind_c...

Do you also consider static types, for loops and exceptions to be "snake oil"?

No, and I don't think they have anything to do with Bret Victor's vision outlined in the article.

If by "change how we code" you mean use Rust for safety guarantees? Then yeah, sure. But that's not how you get to "not putting code into a text editor".

"Visual programming" means "crippled tools" because tooling is at least an order of magnitude harder with a visual language than with text.

As a small example, let's talk about ignoring cosmetic details in a program.

How do you do that with text? You strip whitespace, comments perhaps, and you have a pretty good approximation short of building a syntax graph.

How do you do that with flow charts? How do you "strip" purple diamonds versus green boxes? Is the shape cosmetic? The length of line? What about dashed lines, are those semantically meaningful? What about the layout? Do leftmost lines take precedence or can you rearrange the order of edges? Or are the edges labelled somehow to specify precedence?

What does this all mean? Well, it's possible to come up with really compelling demoware. So it's easy to write an article or pitch a concept. But writing a commonly understood visual programming language is hard because we don't really have visual languages, full stop. The closest thing we have are mostly-universal signage, but that's just about tagging matter and locations, not about communicating complex thoughts about procedures.

Yeah I'm not a fan of visual programming, but visualizing effects of programs to help with reasoning, I'm a fan of that. Proofs is my approach, but as humans we don't deal with proofs as text well and have things like sequent calculus and semantic tableau that are amazing aids to reasoning.

Humans can read and write proofs just fine, if they are taught how to.

The problem is that the proofs that one finds in typical math papers are very different from the proofs for computer programs.

Proofs in math papers are "mostly right" about rather complicated facts. This means that what is shown is highly non-trivial, but when an error is found, it rather does not matter since it is rather easy to fix the hole in the proof. The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error.

Proofs for computer programs rather prove statements that are rather trivial and obvious, but very subtle in the edge cases. Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Thus there is typically no way around formalizing it - which with today's tools is very tedious and boring.

> The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error.

Rather than “redundancy”, it's a matter of having nice (algebraic, geometric, whatever) structure. Of course, a pure mathematician has more freedom than a programmer to decide what kinds of structures he wants to work with.

> statements that are rather trivial and obvious, but very subtle in the edge cases.

This is a contradiction in terms. If it seems “trivial and obvious”, but is actually “subtle in the edge cases”, then you are underestimating its complexity.

> Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons.

Then you need to roll up your sleeves and actually prove things, not just skim through purported proofs.

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 actually doing, no matter whether it's formally equivalent or not.

Tools for checking the correctness of desired properties? I can agree with you there; better tools for doing so would be useful. So far, the problem tends to be that the tools are less generally useful than the tools' authors and proponents think they are.

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.

For static analysis, OK. For a compiler, OK. But I want the static analyzer and the compiler to do that so that I don't have to - I don't want to have to think in set theory to program.

And in saying that, I see that I was probably unfair to haskellandchill's point. The claim wasn't that I needed set theory; the claim was that the tools needed it (at least, so it appears to me on re-reading).

Not every program property of interest can be (conveniently) verified using automated tools - especially if your verification tool is a type checker! Sometimes you need to roll up your sleeves and prove things yourself. (Which, by the way, isn't always a bad thing.)

That being said, hopefully you won't have to use set theory, where any structure that actually matters to you has to be encoded in terms of sets containing sets containing sets, until you reach turtles.

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.

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.

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...

If FireFox provided a formal model of how it lays things out I can prove I use it correctly in my code. It's about trust and providing models for other programmers to use in their proofs along with our code. Or code and proofs can be even more intertwined, since they are very related.

Interesting point.

It's hard to prove theorems without the [correct] axioms.

I suppose what our field needs to do is some "triage" categorizing aspects of systems that MUST be "defined and proven" vs those that can be "intuited" - e.g. - back-end database updates need to be correct, but it's acceptable to have the user reload a web page if something crashes occasionally???

But The Man wants lots of 'wares made by cheap full stack developers, er, dev-ops :-(

> 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.

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 don't see how set theory & etc could have led to any different outcome here.

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.

It goes beyond perception; I think there's something missing, and I think someone is close to finding it.

Databases are already employing logic and set theory to great effect (whether practitioners realize it or not). The fact that you can write a few dozen lines of SQL in a few minutes, and run it over millions of records, and feel confident in the results is astounding.

But there are other types of programming where it has not been so successful. I'm trying to learn some TLA+, and I'd like to see if it can help model resource management/lifetimes.

I think rust is very promising because it brings a lot of PL ideas into a practical setting. One of the best ideas they had was to make it not depend on a runtime, so you could use it without reinventing the world.

> 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).

Reply on news.ycombinator.com