261–270 of 274 posts
"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…
Earlier quoted context omitted.
Is TLA+ pseudocode? It doesn't actually do anything, right? Your example with updating servers, it will never actually update the servers, right? After you try it out in TLA+, you still have to write the real code in some other language, like Bash. If so, then isn't there still a risk of bugs in your Bash program, from typos, leaving out something from the TLA+ plan, or otherwise miscopying it? If so, TLA+ does less…
Yeah, TLA+ just verifies the spec, not the actual code. You still need to write tests and use code review and the like.
"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…
By the way the article makes another similar mistake: "Instead of writing normal programming code, you created a model of the system’s behavior" and then it talks about how programmers like to code and oppose this new approach - but this model creation is still coding - the code is visual and a little bit more high level. But building this model is still programming.
Earlier quoted context omitted.
I remain open-minded to the idea that category theory could help me make better computer programs, but I have yet to see anything that suggests to me that it really would. FWIW, I understand how monads work in Haskell & co, and I definitely see their value. But I don't consider myself to know any category theory at all.
SQL and category theory have a fair degree of overlap so there is that.
This article is silly in a lot of ways. The real problem of software engineering is not "how do you prove this code follows algorithm X exactly?" It's "how do you know what algorithm X needs to be in sufficient detail to implement it?" It's "when you realize you were wrong about algorithm X, how do you change your existing, working code to implement the new algorithm X-prime, without interruption?" It's "what do we d…
Everything you said after "this article is silly" kinda seems like just restating the exact point of the article. The central idea is that the massive costs of writing code that adheres to a specification takes away resources from the task of understanding the problem space well enough to create a correct specification. That is, incidental complexity overwhelms essential complexity in modern software engineering. The…
"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…
Programming is making the detailed plans - the building phase the one that is analogue to the brick laying or hammering nails is done by the compiler. Of course this is not an argument against making less detailed, more overall sketches - they are still useful - it is only that that particular argument for it is incorrect. By the way the article makes another similar mistake: "Instead of writing normal programming co…
I agree with you, but I don't think this is a mistake in the article. I read it as normal programming code meaning low level procedures as are typically written these days.
Earlier quoted context omitted.
In the history of the Bell System, no electromechanical exchange was ever totally down for more than half an hour for any reason other than an natural disaster.
Someday I should write up how that was done in modern terminology. You can read the "Number 5 Crossbar" documents, but the terminology is archaic.[1] Crossbar offices consisted of a dumb switching fabric and lots of microservices. The switching fabric did the actual connecting, but it was told what to connect by other hardware. Each microservice was implemented on special-purpose hardware, and there were always at le…
"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…
Exactly. This is ignoring the fact that code is a more useful blueprint than anything else for programs. I'm sure if architects had the ability to magically conjure building materials out of thin air and try things in real life for free, architecture would involve a lot more trying and a lot less planning. Of course, I'm sure the article is talking about people just rushing into production code without thought, and I…
This is so clearly false that it can actually be mathematically disproven. To prove that there are better software blueprints than code, I will prove that there exist algorithms/systems for which sufficient formal blueprints exist, yet no code can capture. To prove that, I will need to define the terms more precisely. A "sufficient blueprint" is one that makes it possible to prove properties of interest about your software. "Code" is a formal representation of an algorithm, which always allows efficient mechanical execution, meaning, mechanically executing code is within a polynomial bound of the complexity of the algorithm that code expresses.
Now for the counterexamle: take the specification of the Quicksort algorithm, [1], shortened here as: 1. Pick a pivot. 2. Partition the elements around the pivot. 3. Recursively apply 1 and 2 to the resulting partitions.
I claim that this specification is sufficient. For example, from a direct formal statement of it, you can formally prove that it actually sorts and that it runs in worst-case quadratic time complexity. Yet, I claim that no code can express the above specification; in fact, no code can express any of the three steps. For example, step 1 says "pick a pivot", but it doesn't say which. This is not an omission. It doesn't say which because it doesn't matter -- any choice will do. And yet, code must necessarily say which pivot to pick, and when it does, it is no longer captures the specification, and is no longer a blueprint for all implementations of that specification. Similarly for the other two steps: code must specify which partitions are created of the very many possible and completely fine ones, and in what order the recursion takes place. QED
Languages like TLA+ can formally, i.e., mathematically, capture precisely the specification above and express anything code can. There is no magic here: Efficient execution of code (provably!) cannot be done in the presence of some quantifiers, yet quantifiers increase the expressiveness and "generality" of the language.
Anyway, TLA+ and Formal Methods seem a promising thing and definitely need to check that out. I totally agree with him with the way we are not giving a good weight to planning especially for applications that need robust security and safety. Especially after the appearance of Agile methodology and alike. (no system is perfect anyway) But definitely we need more of that verification and we don't need it in the esoteric way they mentioned but in the easy way that allows every programmer to use without so much complexity. Maybe tooling around something like TLA+ could make it easier to understand. People in here though say that it's not that hard but it's not beneficial in every single situation just when you have complex algorithms.
I got convinced though with another idea that's easier to apply at least for now, using type systems (type theory) through using a programming language with sound type system (Facebook is making nice progress in that) on the front end FB made ReasonML , a language derived from OCaml to generate javascript. It really erases a whole set of bugs by getting a good type system like that. I'm learning these days OCaml and Reason. New languages as Rust are doing great too. I think writing code is improving these days but it'll get definitely better in the future as we understand more about how we actually do it. The field is just around 70 years old and it's still in its infancy I think.
This sounds remarkably similar to the ambition of the Logo language (from 1967):