This is not something to be celebrated. This is more typical hacker brute force engineering that co-opts the name of the engineering style for making safety critical systems without the essence of the actual engineering process. Space shuttle engineers use formal methods, they don’t just brute force their way to the control system of the most advanced piece of technology humans have ever developed by sprinkling a bunch of if/else statements and then calling it done. If space shuttle engineering was just a matter of covering every case then every single beginning software engineer is technically a space shuttle engineer. So really this should be called “beginner engineering style”.
Maybe I’m being more angry than necessary but the consistent lack of real understanding prevalent in SV hacker circles starts to grate on you after a certain point and this is yet another example of it.
Do you have some info on the use of formal methods? From memory they used ada and had a consensus model of computation but I don’t remember reading anything about formal methods being used.
The entire engineering team for the Apollo missions consisted of mathematicians. The most famous of them being Margaret Hamilton
Her areas of expertise include systems design and software development, enterprise and process modelling, development paradigm, formal systems modeling languages, system-oriented objects for systems modelling and development, automated life-cycle environments, methods for maximizing software reliability and reuse, domain analysis, correctness by built-in language properties, open-architecture techniques for robust systems, full life-cycle automation, quality assurance, seamless integration, error detection and recovery techniques, man-machine interface systems, operating systems, end-to-end testing techniques, and life-cycle management techniques.
The Wikipedia article for her includes more information about her and the team that set the precedent for all software engineering at NASA. Having been trained as a mathematician in a previous life I can assure you they used formal methods. Digging up the actual historical artifacts is left as an exercise for the reader.
So a mathematician that invented the term “software engineering”, who had formal training in rigorous proof, who founded a company based on formal methods, who along with her team set all the precedents that all software engineers at NASA use does not count as evidence?
This is the thing that gets me about software folks, you could have literally googled “Margaret Hamilton formal methods” and would have stumbled on all her work: https://www.researchgate.net/scientific-contributions/70768706_Margaret_Hamilton. Instead you chose a denigrating response when all the inferential evidence pointed to the validity of formal methods being used to develop the Apollo guidance system and this work informed all later software work at NASA. So ya, I have sources and it was a single google search away.
Did you follow that link? Did you look at the titles and the dates?
Date: January 1974
Title: Higher order software techniques applied to a space shuttle prototype program.
Abstract: HOS concepts are now being applied to a prototype Shuttle flight software system. By providing software with its own meta-software and its own universal system, not only can we produce reliable systems, but we can also communicate these systems to others. Development and real-time flexibility are not sacrificed. The only limitations applied are those which prevent a potential error from occuring, i. e., the only flexibility missing is that which allows for flexibility of errors.
I have thought about this a lot recently since I picked up writing some Java code in an IDE when I am normally a VIM + Python/etc person.
Turns out that (for me) the tooling determines what is more comfortable. WIth Java and an IDE, I have started to pick up using the IDE to do a lot of things for me and I navigate the code by classes and method names (CTRL-click etc). Before I used an IDE, I found most Java codebases insane, now I am writing such a thing for myself :)
With a text editor, I did rely much more on ctags and search strings for browsing through the code. In that working mode larger files are nicer to work with actually, because you have everything quickly reachable with the search functionality of the editor.
So far my personal observations. I do think that a lot of other devs can relate.
I wonder what a software engineer for spacecrafts would say about it. I do think they would have an opinion and I wonder whether this is indeed Spacecraft-style. I hope they have a test suite that covers all the cases they explicitly treat.
Of course I have been in similar situations when a piece of code was written in a way that kind of gave a lot of new hires an itch for a rewrite (that made things worse usually). I have also rewritten stuff that others said had no potential to become a cleaner piece of code (sometimes I was sucessful even). I think it might be a bit more honest not to argue that the piece of code is as best as it can be, but just to say “we don’t want to spend refactoring and review efforts on this file unless they are warranted by bugs or feature requests”.
They Write the Right Stuff details the modern crew. The “Apollo Beginnings” part of this paper (pdf) describes the early approach to low-defect by the people responsible for verification. If anything, it’s rigorous methods that focus lots on understanding exactly what the software will do with lots of docs, collaboration, and analysis/testing.
I find it interesting that it’s so strict about things like “always require else”, but they allow if !found … else … (logically simpler is if found … else …).
Also, this whole idea makes me happy. I’ve become an advocate for more verbose programming over the past few years. Typing on the keyboard is literally the cheapest thing I do at work. It confounds me that people what to make code harder to read so they can save a few keystrokes.
If verbosity and understandability were the same thing, I’d agree. Verbosity gives you more to read. You can hone in on particulars. But I notice that when you get used to some terseness, you can see the particulars in context.
Isn’t the crux of the issue here the intended audience? If you don’t know who’s going to be reading your code you ought to err on the side of verbosity, ISTM.
Let’s say that you are a very junior developer and you encounter a library function you’ve never seen before. You want to understand the code so you look up that function. Once you learn it, you discover that you can use it in many places and remove a lot of boiler-plate code the next time you do something similar.
Believe it or not, for some people that function is ‘map.’ That’s the “inspiration to learn” I was talking about.
This is true, but again, you have to take the audience into consideration. Do you intend the code to be instructive as well as functional? Not all code needs or ought to be so.
Seeing less code makes people brave – if they believe they can understand what they see, they often assume they can understand what they don’t see.
If that code isn’t relevant, then it might be ok, but if the code is relevant, you’re setting them up for failure.
That’s why generally you’ll be more successful giving them as little to read as necessary.
That qualifier “necessary” is tricky because sometimes seeing an algorithm “spelled out” makes it easier to understand – and I suspect your experiences are more like this. Here’s a situation where spelling it out is a disaster waiting to happen:
I’ve got some code at the moment that unwinds tags and then performs an intrinsic operation on them, or calls the nested function. Just handing the intrinsic operation looks something like this (all unrolled):
#define FOR(n,a) {size_t i=0,_n=(n);for(;i<_n;++i){a}}
#define TAGGED(x) (((uintptr_t)(x))&1)
#define UNTAG(x) (((intptr_t)(x))>>1)
#define MAKE_TAGGED(x) ((A)((((intptr_t)(x))<<1)|1))
#define F(f,O) A f(A x,A y){ A r;\
if(TAGGED(x)&&TAGGED(y))return MAKE_TAGGED(UNTAG(x) O UNTAG(y)); \
if(TAGGED(x)){ \
if(y->ref == 0){ FOR(y->size,y->data[i] = UNTAG(x) O y->data[i]); return y; } \
r = make(y->size); FOR(r->size, r->data[i] = UNTAG(x) O y->data[i]); unref(y); return r; }} \
if(TAGGED(y)){ \
if(x->ref == 0) { FOR(x->size,x->data[i] O ## = UNTAG(y)); return x; } \
r = make(x->size); FOR(r->size, r->data[i] = x->data[i] O UNTAG(y)); unref(x); return r; }} \
if(x->size != y->size) return ERROR_SIZE; \
if(!x->ref) { FOR(x->size,x->data[i] = x->data[i] O y->data[i]); unref(y); return x; } \
if(!y->ref) { FOR(x->size,y->data[i] = x->data[i] O y->data[i]); unref(x); return y; } \
r = make(x->size); FOR(r->size, r->data[i] = x->data[i] O UNTAG(y)); unref(x); unref(y); return r; }
Note I want to check the reference count and reuse any object whenever possible since they could be very large (multi-terabyte!) so I save a lot of RAM/swapping here. However as I mentioned I also need a check for whether the object is a nested array. “A” is my array type and it looks like this:
struct A;typedef struct A*A;struct A{ int is_data, ref; size_t size; union { long long data[1]; A members[1]; }};
That means each of the untagged paths above also need a:
if(!x->is_data){ /* repeat above for f(X,Y) instead of X O Y */ }
This quickly gets this mere macro larger than a screen – and in the real implementation, I have about twenty types (not just data and array, and some of those types require prep on the arguments, e.g. are timestamps) or so that I want constructed implementations for. Madness! Testing all those combinations is really hard, and it’s too big to read (is there a bug in the above? There could be!)
The only way I can keep the code understandable is to be less verbose. In my case that means a few macros, load some temporary variables, and rely on gcc to eliminate the dead loads and built optimised assembly (it does).
But what’s the intended audience of the code above? Is it fellow practitioners, or is it more workaday journeymen like myself? If the problem is genuinely complex, the solution will also be complex – and it is, as you say, a positive good not to try and obfuscate the complexity.
I guess my point is, there is no single rule that encompasses all cases, but a useful heuristic for me in my career has been to constrain the code I’m writing to the capabilities of the expected audience. My greatest failures have come when I’ve ignored this advice to myself.
The crux of it is this: maintainability. The intended audience is ‘anyone and everyone who reads this code and has to work on it now and in the future’.
Confuscated, difficult to understand code is another thing. In this case, control over the codebase is usually the issue. You can’t have high-performance, expensive things, without control.
It seems to me there’d be a place for a tool which allowed the viewer to hide/display comments at different levels, similar to filtering on logging levels.
This is not something to be celebrated. This is more typical hacker brute force engineering that co-opts the name of the engineering style for making safety critical systems without the essence of the actual engineering process. Space shuttle engineers use formal methods, they don’t just brute force their way to the control system of the most advanced piece of technology humans have ever developed by sprinkling a bunch of if/else statements and then calling it done. If space shuttle engineering was just a matter of covering every case then every single beginning software engineer is technically a space shuttle engineer. So really this should be called “beginner engineering style”.
Maybe I’m being more angry than necessary but the consistent lack of real understanding prevalent in SV hacker circles starts to grate on you after a certain point and this is yet another example of it.
Do you have some info on the use of formal methods? From memory they used ada and had a consensus model of computation but I don’t remember reading anything about formal methods being used.
The entire engineering team for the Apollo missions consisted of mathematicians. The most famous of them being Margaret Hamilton
The Wikipedia article for her includes more information about her and the team that set the precedent for all software engineering at NASA. Having been trained as a mathematician in a previous life I can assure you they used formal methods. Digging up the actual historical artifacts is left as an exercise for the reader.
If you have no sources just say so.
Here is an article talking about first use of formal methods in Nasa15 years after the bulk of the space shuttle code was done: https://link.springer.com/article/10.1023/A:1008693709419
If you have some actual information feel free to share it.
So a mathematician that invented the term “software engineering”, who had formal training in rigorous proof, who founded a company based on formal methods, who along with her team set all the precedents that all software engineers at NASA use does not count as evidence?
This is the thing that gets me about software folks, you could have literally googled “Margaret Hamilton formal methods” and would have stumbled on all her work: https://www.researchgate.net/scientific-contributions/70768706_Margaret_Hamilton. Instead you chose a denigrating response when all the inferential evidence pointed to the validity of formal methods being used to develop the Apollo guidance system and this work informed all later software work at NASA. So ya, I have sources and it was a single google search away.
I’m asking for some information about the use of formal methods in the space shuttle. I googled it and I found nothing.
Do you have any information specifically about it or not?
Did you follow that link? Did you look at the titles and the dates?
Date: January 1974
Title: Higher order software techniques applied to a space shuttle prototype program.
Abstract: HOS concepts are now being applied to a prototype Shuttle flight software system. By providing software with its own meta-software and its own universal system, not only can we produce reliable systems, but we can also communicate these systems to others. Development and real-time flexibility are not sacrificed. The only limitations applied are those which prevent a potential error from occuring, i. e., the only flexibility missing is that which allows for flexibility of errors.
https://www.researchgate.net/publication/221534858_Higher_order_software_techniques_applied_to_a_space_shuttle_prototype_program
That says prototype. Did they use it on the real thing? If they did how and if they didn’t why not?
Maybe I’m a bad programmer, but I just can not cope with modules with over a thousand lines. It’s just too daunting,
I have thought about this a lot recently since I picked up writing some Java code in an IDE when I am normally a VIM + Python/etc person.
Turns out that (for me) the tooling determines what is more comfortable. WIth Java and an IDE, I have started to pick up using the IDE to do a lot of things for me and I navigate the code by classes and method names (CTRL-click etc). Before I used an IDE, I found most Java codebases insane, now I am writing such a thing for myself :)
With a text editor, I did rely much more on ctags and search strings for browsing through the code. In that working mode larger files are nicer to work with actually, because you have everything quickly reachable with the search functionality of the editor.
So far my personal observations. I do think that a lot of other devs can relate.
VIM surely has an extension which will do this for you. I know emacs does.
Exuberant ctags + FZF has worked wonders for me :)
Isn’t there something language-server based?
Sometimes it’s nice to grep for the start of constructs like function declarations and control structures to get a sense of what is going on.
https://paste.ee/p/g8N83
I wonder what a software engineer for spacecrafts would say about it. I do think they would have an opinion and I wonder whether this is indeed Spacecraft-style. I hope they have a test suite that covers all the cases they explicitly treat.
Of course I have been in similar situations when a piece of code was written in a way that kind of gave a lot of new hires an itch for a rewrite (that made things worse usually). I have also rewritten stuff that others said had no potential to become a cleaner piece of code (sometimes I was sucessful even). I think it might be a bit more honest not to argue that the piece of code is as best as it can be, but just to say “we don’t want to spend refactoring and review efforts on this file unless they are warranted by bugs or feature requests”.
They Write the Right Stuff details the modern crew. The “Apollo Beginnings” part of this paper (pdf) describes the early approach to low-defect by the people responsible for verification. If anything, it’s rigorous methods that focus lots on understanding exactly what the software will do with lots of docs, collaboration, and analysis/testing.
I’d love to see this re-implemented with the Go 2 error handling proposal, and see if correctness was made any easier.
I find it interesting that it’s so strict about things like “always require else”, but they allow
if !found … else …(logically simpler isif found … else …).Also, this whole idea makes me happy. I’ve become an advocate for more verbose programming over the past few years. Typing on the keyboard is literally the cheapest thing I do at work. It confounds me that people what to make code harder to read so they can save a few keystrokes.
If verbosity and understandability were the same thing, I’d agree. Verbosity gives you more to read. You can hone in on particulars. But I notice that when you get used to some terseness, you can see the particulars in context.
Isn’t the crux of the issue here the intended audience? If you don’t know who’s going to be reading your code you ought to err on the side of verbosity, ISTM.
We can write at a level that inspires people to learn.
If shit is actively hitting the fan and I need to fix the damn code, I don’t want to be handed something that “inspires me to learn”.
I want something I can grasp, understand what it does and why and figure out the problem.
I can get inspired and learn on my own dime, not when I’m maintaining a broken piece of code.
Let’s say that you are a very junior developer and you encounter a library function you’ve never seen before. You want to understand the code so you look up that function. Once you learn it, you discover that you can use it in many places and remove a lot of boiler-plate code the next time you do something similar.
Believe it or not, for some people that function is ‘map.’ That’s the “inspiration to learn” I was talking about.
This is true, but again, you have to take the audience into consideration. Do you intend the code to be instructive as well as functional? Not all code needs or ought to be so.
Verbosity means you can see less code at a time.
Seeing less code makes people brave – if they believe they can understand what they see, they often assume they can understand what they don’t see.
If that code isn’t relevant, then it might be ok, but if the code is relevant, you’re setting them up for failure.
That’s why generally you’ll be more successful giving them as little to read as necessary.
That qualifier “necessary” is tricky because sometimes seeing an algorithm “spelled out” makes it easier to understand – and I suspect your experiences are more like this. Here’s a situation where spelling it out is a disaster waiting to happen:
I’ve got some code at the moment that unwinds tags and then performs an intrinsic operation on them, or calls the nested function. Just handing the intrinsic operation looks something like this (all unrolled):
Note I want to check the reference count and reuse any object whenever possible since they could be very large (multi-terabyte!) so I save a lot of RAM/swapping here. However as I mentioned I also need a check for whether the object is a nested array. “A” is my array type and it looks like this:
That means each of the untagged paths above also need a:
This quickly gets this mere macro larger than a screen – and in the real implementation, I have about twenty types (not just data and array, and some of those types require prep on the arguments, e.g. are timestamps) or so that I want constructed implementations for. Madness! Testing all those combinations is really hard, and it’s too big to read (is there a bug in the above? There could be!)
The only way I can keep the code understandable is to be less verbose. In my case that means a few macros, load some temporary variables, and rely on gcc to eliminate the dead loads and built optimised assembly (it does).
But what’s the intended audience of the code above? Is it fellow practitioners, or is it more workaday journeymen like myself? If the problem is genuinely complex, the solution will also be complex – and it is, as you say, a positive good not to try and obfuscate the complexity.
I guess my point is, there is no single rule that encompasses all cases, but a useful heuristic for me in my career has been to constrain the code I’m writing to the capabilities of the expected audience. My greatest failures have come when I’ve ignored this advice to myself.
The crux of it is this: maintainability. The intended audience is ‘anyone and everyone who reads this code and has to work on it now and in the future’.
Confuscated, difficult to understand code is another thing. In this case, control over the codebase is usually the issue. You can’t have high-performance, expensive things, without control.
It seems to me there’d be a place for a tool which allowed the viewer to hide/display comments at different levels, similar to filtering on logging levels.
I like this. Sort of easier to read in other languages. Thinking of Rust, one would greatly benefit from match statements and Result types.