4 ms·

Critical embedded systems for avionics and robotics systems frequently deal with values that must be within a certain range. Runtime bounds checking can be too

Critical embedded systems for avionics and robotics systems frequently deal with values that must be within a certain range. Runtime bounds checking can be too expensive in these environments and dependent types would allow for provably correct bounded integers without checks. That is actually a problem I am dealing with right now in some MIL-STD-1553 data bus code. While I was at NASA I was advocating for using Rust instead of C/C++ and FORTRAN and many people were interested because of the safety/performance aspects. I think it would take some serious ground from them in that area with dependent types also.

yawaramin 7y ago
In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language, SPARK, it can prove things like array bounds (and I assume integer bounds) are respected, without runtime checks. See e.g. https://www.adacore.com/gems/gem-68 https://www.adacore.com/gems/gem-68 The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.
mikekchar 7y ago
Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-value. For another example, imagine subtracting something from an unsigned int. You need to ensure that the value never goes below zero If you have an expression like 'x - 1', then the compiler needs to ensure that x is always > 0. The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen. I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)

yawaramin 7y ago

In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language, SPARK, it can prove things like array bounds (and I assume integer bounds) are respected, without runtime checks. See e.g. https://www.adacore.com/gems/gem-68 https://www.adacore.com/gems/gem-68 The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.

mikekchar 7y ago

Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-value. For another example, imagine subtracting something from an unsigned int. You need to ensure that the value never goes below zero If you have an expression like 'x - 1', then the compiler needs to ensure that x is always > 0. The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen. I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)