4 ms·

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

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_cyber_warfare https://www.ted.com/talks/chris_domas_the_1s_and_0s_behind_c...

woah 9y ago
Do you also consider static types, for loops and exceptions to be "snake oil"?
- Bartweiss 9y ago
  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".
humanrebar 9y ago
"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.
haskellandchill 9y ago
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.
- catnaroek 9y ago
  Humans can read and write proofs just fine, if they are taught how to.
  - wolfgke 9y ago
    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.
    - catnaroek 9y ago
      > 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.

woah 9y ago

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

Bartweiss 9y ago
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".

humanrebar 9y ago

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

haskellandchill 9y ago

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.

catnaroek 9y ago
Humans can read and write proofs just fine, if they are taught how to.
- wolfgke 9y ago
  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.
  - catnaroek 9y ago
    > 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.