5 ms·

I’ve wanted to try Ada and Spark for a while mainly to try formal verification and because a professor I listened to for a while keep banging on that most bugs

I’ve wanted to try Ada and Spark for a while mainly to try formal verification and because a professor I listened to for a while keep banging on that most bugs don’t need to be written if you use Ada properly. (Shrug.) Who knows, I’d like to try it sometime.

traceroute66 5y ago
> most bugs don’t need to be written if you use Ada properly. I think both Airbus and Boeing have been doing their best to demonstrate the limitations of Ada and Spark.
- ajxs 5y ago
  Ironically, you're right. Given the incredibly strict regulatory environment they work within, and the incredibly small margin of error, the fact that two of the biggest manufacturers of commercial aircraft choose to use Ada/Spark speaks volumes.
  - msla 5y ago
    How many fewer bugs would they have if they used a language with a real type system, like Haskell?
StreamBright 5y ago
Your professor was assuming most bugs are bugs that Ada language features protect against?
bluGill 5y ago
C++ is probably going to get contract support which if it works out will allow the same tools. I've read the latest paper, it isn't as powerful as Spark, but should get there.
- pjmlp 5y ago
  Lets see if it has better luck than the version that was temporarly accepted in C++20.
  - bluGill 5y ago
    Well the people doing it did learn lessons from that. Only time will tell of course.
- gavinray 5y ago
  Not trying to start a war, but do you genuinely believe that C++ even with solid contracts is a conducive environment to bug-free programming? I am not very familiar with it (have published 1 small library and 1 PR to a large, popular framework), but when learning the language after having written most other things it felt like it had the most footguns and number of random rules you had to memorize + instances of undefined behavior. I've never published anything with Ada (mostly because almost nobody uses it, so I've not had the same practical usecases) but I do follow the language passively and have experimented with it. I feel much more comfortable that I could write a correct Ada program than a correct C++ program. I think I could write C++ for 5 years and not feel sure my program is entirely correct, even with IE "cppcheck", "clang-static-analyzer", "ASAN/TSAN/UBSAN" etc.
  - bluGill 5y ago
    Very qualified yes. First, contracts are step one: they enable additional tools that can do static formal proofs using those contracts. It is impossible to prove anything about code that has a buffer overlow. In theory we have can write those tools without contracts, but the runtime for anything more than helloworld is unacceptable so nobody has even written them, contracts are believed to help bring that under control. second, I assume only the latest modern C++ is used. I expect tools to give up as soon as they see constructs that are hard to analyze. (new/delete is obvious - but they reserve the right to add more constraints) Third, modern C++ if you stick to only that is a lot easier to write safe code than C++98. Things are getting better - or where they are not we can treat them like rust treats unsafe - sometimes you need to do tricky things that tools can work with: isolate them to only those areas, have your best write the code, test it hard, and pray they work. Fourth, conductive to bug free development is relative. I won't claim C++ will be the most conductive to bug free code. Part of that is intentional: C++ aims to be useful in places where you are willing to make trade offs - if you are not willing to trade at least some productivity for runtime speed C++ is not the right language for you. Note the last: I never claimed it will be better than Ada/Rust/whatever. I have no experience with either, but tend to believe those who claim they are more productive. I maintain a lot of C++, which interoperates with other C++: adding another language is probably lower productivity than writing more C++ in the long run just because those interfaces between languages tend to be where things are the hardest. So I'm taking a different approach: getting involved with the C++ standard to attempt to make it more productive.

traceroute66 5y ago

> most bugs don’t need to be written if you use Ada properly. I think both Airbus and Boeing have been doing their best to demonstrate the limitations of Ada and Spark.

ajxs 5y ago
Ironically, you're right. Given the incredibly strict regulatory environment they work within, and the incredibly small margin of error, the fact that two of the biggest manufacturers of commercial aircraft choose to use Ada/Spark speaks volumes.
- msla 5y ago
  How many fewer bugs would they have if they used a language with a real type system, like Haskell?

StreamBright 5y ago

Your professor was assuming most bugs are bugs that Ada language features protect against?

bluGill 5y ago

C++ is probably going to get contract support which if it works out will allow the same tools. I've read the latest paper, it isn't as powerful as Spark, but should get there.

pjmlp 5y ago
Lets see if it has better luck than the version that was temporarly accepted in C++20.
- bluGill 5y ago
  Well the people doing it did learn lessons from that. Only time will tell of course.
gavinray 5y ago
Not trying to start a war, but do you genuinely believe that C++ even with solid contracts is a conducive environment to bug-free programming? I am not very familiar with it (have published 1 small library and 1 PR to a large, popular framework), but when learning the language after having written most other things it felt like it had the most footguns and number of random rules you had to memorize + instances of undefined behavior. I've never published anything with Ada (mostly because almost nobody uses it, so I've not had the same practical usecases) but I do follow the language passively and have experimented with it. I feel much more comfortable that I could write a correct Ada program than a correct C++ program. I think I could write C++ for 5 years and not feel sure my program is entirely correct, even with IE "cppcheck", "clang-static-analyzer", "ASAN/TSAN/UBSAN" etc.
- bluGill 5y ago
  Very qualified yes. First, contracts are step one: they enable additional tools that can do static formal proofs using those contracts. It is impossible to prove anything about code that has a buffer overlow. In theory we have can write those tools without contracts, but the runtime for anything more than helloworld is unacceptable so nobody has even written them, contracts are believed to help bring that under control. second, I assume only the latest modern C++ is used. I expect tools to give up as soon as they see constructs that are hard to analyze. (new/delete is obvious - but they reserve the right to add more constraints) Third, modern C++ if you stick to only that is a lot easier to write safe code than C++98. Things are getting better - or where they are not we can treat them like rust treats unsafe - sometimes you need to do tricky things that tools can work with: isolate them to only those areas, have your best write the code, test it hard, and pray they work. Fourth, conductive to bug free development is relative. I won't claim C++ will be the most conductive to bug free code. Part of that is intentional: C++ aims to be useful in places where you are willing to make trade offs - if you are not willing to trade at least some productivity for runtime speed C++ is not the right language for you. Note the last: I never claimed it will be better than Ada/Rust/whatever. I have no experience with either, but tend to believe those who claim they are more productive. I maintain a lot of C++, which interoperates with other C++: adding another language is probably lower productivity than writing more C++ in the long run just because those interfaces between languages tend to be where things are the hardest. So I'm taking a different approach: getting involved with the C++ standard to attempt to make it more productive.