One of the best arguments for Lisp I've heard this decade
Programmers who want to change how we code before catastrophe strikes
181–190 of 274 posts
Re: Programmers who want to change how we code before catastrophe strikes
#182"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…
"Everything should be built top-down, except the first time" --Alan Perlis
Re: Programmers who want to change how we code before catastrophe strikes
#183Disappointing to see such a long article and no mention of type theory, or any other work from the "correct by construction" school of formal methods. It's all normie model checking, TLA+ etc.
Type theory is much less than "correct by construction" formal methods. Type theory is great at preventing a whole class of bugs (an operation on a value for which that operation doesn't make sense). But it's inadequate for the larger problem, of whether the operation is the correct one. Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the fo…
> And you have the little problem of (correctly) creating the formal spec.
How on Earth did we end up putting people who can't write down precisely what they want in charge of programming machines that do exactly what you tell them to?
Re: Programmers who want to change how we code before catastrophe strikes
#184Programmers write code badly due to time constraints in many cases or really disconnected teams being led by business not engineering.
Rarely is budget allotted for quality code, you have to fight for it as a coder to your own detriment internally on timelines/shipping.
Engineer led companies, or companies that value engineering as a main decision maker in the company usually fare better with issues like this and are already smart about design, architecture, standards, security, reliability, interoperability, user experience and more.
Re: Programmers who want to change how we code before catastrophe strikes
#185Earlier quoted context omitted.
Me too. The very few design specs I've seen during my 15+ yrs as a programmer are typically high-level enough to be the mechanical equivalent of "cogs needed here, and springs!". What kind of cogs, e.g. diameter, teeth count, diameter of the center hole (should the hole even be in the center?) and what kind of springs are never mentioned. If you ask the customer about functionality their response is "we want it to wo…
This is brilliantly funny, you made my day. In all seriousness though, go find a new job.
[deleted]
Re: Programmers who want to change how we code before catastrophe strikes
#186"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…
Me too. The very few design specs I've seen during my 15+ yrs as a programmer are typically high-level enough to be the mechanical equivalent of "cogs needed here, and springs!". What kind of cogs, e.g. diameter, teeth count, diameter of the center hole (should the hole even be in the center?) and what kind of springs are never mentioned. If you ask the customer about functionality their response is "we want it to wo…
You had me at 'and springs!'
Re: Programmers who want to change how we code before catastrophe strikes
#187This article reports uncritically the plaintiff’s claim that Toyota runaway acceleration issues were a software issue. The Wikipedia article presents a more balanced report; the black box data is particularly interesting.
https://en.wikipedia.org/wiki/2009%E2%80%9311_Toyota_vehicle...
Re: Programmers who want to change how we code before catastrophe strikes
#188"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…
So basically all our problems will go away if we return to UML and requirements documentation that's hundreds of pages long and edited for ages before anyone writes any code.
> So basically all our problems will go away if we return to UML
UML belongs to the class of semiformal models. In other words: It leads people into believing that a lot more things are precisely specified than actually are.
Re: Programmers who want to change how we code before catastrophe strikes
#189Earlier quoted context omitted.
So basically all our problems will go away if we return to UML and requirements documentation that's hundreds of pages long and edited for ages before anyone writes any code.
Thats how most Medical Device software is written :)
I was intern at a company that writes medical software and software for medical devices. I tell you: The usual standards are mostly bureaucracy and rather worthless in that they change anything about development practice.
I also had a nice private talk with a person who worked in software development for avionics at some very well-known company. Before I talked to him, I thought that at least there the development practices are better. After that I seriously ask why there are not serious accidents about everyday and how the plane even comes off ground. :-(
TLDR: Dream on... :-(
Re: Programmers who want to change how we code before catastrophe strikes
#190Earlier quoted context omitted.
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.