Earlier quoted context omitted.
> INRIA is a scary scary place. Why ?
I assume scary as in "scar(il)y smart", in the sense that it's (almost) disturbing to see their sophistication and competence.
Thank you.
Programmers who want to change how we code before catastrophe strikes
91–100 of 274 posts
Re: Programmers who want to change how we code before catastrophe strikes
#92Earlier 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 :)
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.
Re: Programmers who want to change how we code before catastrophe strikes
#93Earlier quoted context omitted.
> maybe it is something to look into for cars, airplanes, medicine, etc. For the rest of us, who still wrestle with complexity but probably would't accidentally kill someone, here are some simpler aids: TLA+ isn't perfect, but it's actually not that hard to use! I'm a webdev and it comes in handy all the time. > Data-driven programming. I'll just quote some really smart people: You might want to check out Alloy. It's…
Can you expand on your process for using TLA+ in web development?
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...
Re: Programmers who want to change how we code before catastrophe strikes
#94Earlier 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 :)
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 Ma…
Do you also consider static types, for loops and exceptions to be "snake oil"?
Re: Programmers who want to change how we code before catastrophe strikes
#95I'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?
It helps in two ways:
1) You have to specify your system, right? With TLA+, you can just wave you hands and say "okay this part does something, I guess." You have to force yourself to understand what, exactly, you want your system to do and what you want out of it.
2) Most systems have edge cases, side effects, and race conditions. Are you sure your design is robust against them? You might think you have good arguments for that, but wouldn't it be better to rigorously _check_?
Tests and types and stuff help you find bugs in your implementation. TLA+ helps you find bugs in your blueprints.
Re: Programmers who want to change how we code before catastrophe strikes
#96Earlier 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 :)
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 Ma…
"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.
Re: Programmers who want to change how we code before catastrophe strikes
#97So. 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.
Re: Programmers who want to change how we code before catastrophe strikes
#98Earlier quoted context omitted.
> 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…
>* 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 unprompted. We also hold them responsible if their bridges fail from some minor, anticipated harm like vandalism or a car cr…
How many software projects have to deal with gravity? Weather patterns? How many software projects need teams of construction workers to actually build?
Different kinds of engineering have different requirements. Just because the challenges in software are different from those in building bridges doesn't mean we get a free pass on correctness.
Re: Programmers who want to change how we code before catastrophe strikes
#99Earlier quoted context omitted.
An excellent framing I saw recently was "I can tell the people who write these articles don't actually want secure code, because they aren't paying me to write it." There's plenty of carefully-written, rigorously-tested code out there. Want to write software for air travel, drug manufacturing, or space flight? You'll have no choice but to write safe, first-rate code. Want a smartphone weather app written to those sta…
Isn't this a tooling and knowledge issue? If I was as productive with TLA+ or model based design as I am with React-Native/Ionic/Swift etc. then we could have a smartphone weather app written to those standards for the same price.
While there's plenty of room for improvement, I legitimately believe that TLA+ is now in a place where it's convenient enough to use in conjunction with Ionic/Swift.
Re: Programmers who want to change how we code before catastrophe strikes
#100Earlier 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 :)
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…
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.