3 ms·

That's why I'd enforce type-hints. The whole story with these critical systems is tricky. At the one hand, they want to have formal verification. Academia real

That's why I'd enforce type-hints. The whole story with these critical systems is tricky. At the one hand, they want to have formal verification. Academia really loves stuff like Haskell for that. There is Ada which was designed with critical systems in mind. On the other hand, there is a lot of C and C++ everywhere. On microcontrollers, no matter how much you love Haskell, Ada or Rust, there might not even be a compiler and probably no HAL. And in the end, all of those languages focus on the machine and the math. A mathematical prove of the correctness of your software is nice, but readable code is too. And the formal verification doesn't save you from making wrong design choices. It doesn't check your logic. No language or tool can do that. But what I believe a language can do for you is help you express your thoughts in such an simple, structured and readable way that the cognitive load is reduced to a minimum, freeing up thought-power to check your logic. A lot of the failures in space that were caused by software weren't actually programming errors like the overflows that allow us to hack everything. There was a Mars Orbiter that crashed because the data was in the wrong format - still the types matched. A lander crashed because they forgot to put in logic to handle invalid sensor data: a broken sensor in the landing led triggered the 'touch-down' signal, the lander believed it landed and cut the chute. Except it really wasn't even close to ground. Using a bit of hyperbole, there is formal verification in Academia on the one side, and people forgetting to design robust logic while trying to figure out pointers on a microcontroller that can only be programmed in C on the other. Static Python. That's my proposal to save the next mission :)

na85 9y ago
I'm failing to see how static Python addresses any of the concerns you listed. In fact you seem to defeat your own argument when you state: >A lot of the failures in space that were caused by software weren't actually programming errors... Indeed this is true. I work in aerospace (though not in a software development role) and I can tell you a lot of shops are using C/C++ for embedded applications with strict style guides to attempt to mitigate the flaws in those languages. I think the fact that many aerospace-related problems aren't due to programming errors says that current practices are working.
nikofeyn 9y ago
but all that seems to be silly. why try to force feed patches to make python something it was in no way designed for? it seems like the completely wrong approach from a design point of view. and your dismissal of the power of type checking systems seems strange. seems weird to say that it doesn't really help when python has nothing of the sort. even a "static python" wouldn't reach the power of some existing systems. even for dynamic languages, python is behind the times for things like that. for example, look at racket versus python. and then there's languages like idris, which go well beyond what even haskell can do. something like idris would be wonderful for critical embedded systems. and if you really want flexibility and a dynamic language, python seems well below lisp/scheme. i would love to see racket and ML-based languages to move towards embedded development over something like python. finally, both lisps/schemes and ML-based languages are very readable. many would argue they are more readable than a language like python. so your implication that type systems incur a readability penalty isn't generally accurate. > But what I believe a language can do for you is help you express your thoughts in such an simple, structured and readable way that the cognitive load is reduced to a minimum, freeing up thought-power to check your logic. basically what i am getting at is that a language like racket or idris fulfill this requirement very strongly, even moreso than python. and additionally, they come with advanced language features that no version of python will ever likely touch on.

na85 9y ago

I'm failing to see how static Python addresses any of the concerns you listed. In fact you seem to defeat your own argument when you state: >A lot of the failures in space that were caused by software weren't actually programming errors... Indeed this is true. I work in aerospace (though not in a software development role) and I can tell you a lot of shops are using C/C++ for embedded applications with strict style guides to attempt to mitigate the flaws in those languages. I think the fact that many aerospace-related problems aren't due to programming errors says that current practices are working.

nikofeyn 9y ago

but all that seems to be silly. why try to force feed patches to make python something it was in no way designed for? it seems like the completely wrong approach from a design point of view. and your dismissal of the power of type checking systems seems strange. seems weird to say that it doesn't really help when python has nothing of the sort. even a "static python" wouldn't reach the power of some existing systems. even for dynamic languages, python is behind the times for things like that. for example, look at racket versus python. and then there's languages like idris, which go well beyond what even haskell can do. something like idris would be wonderful for critical embedded systems. and if you really want flexibility and a dynamic language, python seems well below lisp/scheme. i would love to see racket and ML-based languages to move towards embedded development over something like python. finally, both lisps/schemes and ML-based languages are very readable. many would argue they are more readable than a language like python. so your implication that type systems incur a readability penalty isn't generally accurate. > But what I believe a language can do for you is help you express your thoughts in such an simple, structured and readable way that the cognitive load is reduced to a minimum, freeing up thought-power to check your logic. basically what i am getting at is that a language like racket or idris fulfill this requirement very strongly, even moreso than python. and additionally, they come with advanced language features that no version of python will ever likely touch on.