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...
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".
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.
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.
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.
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.
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 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.
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.
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).
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.
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.
So it seems to me that, if you can make progress on formal methods in your environment, you're not picking low-hanging fruit...
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 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.