9 ms·
> If runtime safety is turned off, you get undefined behavior You already know someone will teach their students to always have it off because its "slower" or
by lionkor 6y ago
> If runtime safety is turned off, you get undefined behavior
You already know someone will teach their students to always have it off because its "slower" or something.
Make something idiot-proof and the world invents a better idiot.
Another language that does safety like this incredibly well is Ada (Ada/SPARK), and I'm unsure why people aren't more hyped about it. So many people hype Rust or Zig or whatever new language, and yet there's an incredibly safe and expressive language that's used in high-reliability applications like missile guidance systems, that nobody seems to talk about.
- pjmlp 6y agoOr Modula-2, NEWP, BASIC, or really most languages that aren't copy paste compatibel with C. Ada suffered from its domain, original price of compilers, and the few UNIX vendors that cared to offer compiler like Sun, it was an additional acquisiation on top of UNIX SDK. Everyone knows that only newbies do coding errors in C, so why spend the extra money? /s
- qayxc 6y ago> Everyone knows that only newbies do coding errors in C, so why spend the extra money? /s The Ariane 5 maiden flight disaster illustrated quite clearly that the choice of language has little influence on the actual correctness of a program. Ada on its own is no better than Pascal in that regard. A formally verified and thoroughly tested MISRA C program can be safer and more correct than a sloppily written Ada program. So the question is indeed not as rhetorical as one might think - why spend the extra money indeed? Isn't it better spent on verification, testing, tooling and culture, which benefits the development regardless of programming language?
- pjmlp 6y agoAriane 5 error was caused by the remaining 30% programming errors when we leave out the 70% of software failures caused by C typical errors. So yes, it is quite worthy to reduce the amount of money spent in verification, testing, tooling and culture. The alternative is to just give up that programmers will never learn and just force verification at hardware level, like Google is doing on Android. "Memory Tagging for the Kernel: Tag-Based KASAN" https://www.youtube.com/watch?v=f-Rm7JFsJGI https://www.youtube.com/watch?v=f-Rm7JFsJGI Oracle on Solaris SPARC, https://docs.oracle.com/cd/E37838_01/html/E61059/gqajs.html https://docs.oracle.com/cd/E37838_01/html/E61059/gqajs.html Apple on iOS, https://developer.apple.com/documentation/security/preparing_your_app_to_work_with_pointer_authentication https://developer.apple.com/documentation/security/preparing... Microsoft on Azure Sphere, https://www.microsoft.com/security/blog/2020/11/17/meet-the-microsoft-pluton-processor-the-security-chip-designed-for-the-future-of-windows-pcs/ https://www.microsoft.com/security/blog/2020/11/17/meet-the-...
- messe 6y agoIronically enough, I recall reading that if the overflow hadn't triggered a hardware exception and instead was silently ignored, the first stage would have survived; the code in question had just been carried over from Ariane 4 and was no longer important for the operation of the booster..
- vlovich123 6y agoThat’s not an alternative to memory safety. That’s just a basic security measure even if you write everything in a safe language like Rust or Zig (let alone the fact that you have enormous C/C++ legacy codebases that are likely still seeing ongoing development due to switching costs). The reason is you will always have some amount of unsafe code when dealing with the hardware and this is a hardening measure to protect against slipups.
- kjs3 6y agoNo. The Ariane 5 disaster was caused by a development team deliberately turning off safety checks. Ada is in all regards a 'safer' language than Pascal, as long as you don't disable the safety features. http://www-users.math.umn.edu/~arnold/disasters/ariane5rep.html http://www-users.math.umn.edu/~arnold/disasters/ariane5rep.h... http://www.adapower.com/index.php?Command=Class&ClassID=FAQ&CID=328 http://www.adapower.com/index.php?Command=Class&ClassID=FAQ&...
- tored 6y agoIs anyone actively using Modula-2? Actively as in starting new projects, compiler improvements, tooling, community etc.
- pjmlp 6y agoThe GNU M2 compiler is kept up to date with GCC, it is just kept out of tree. https://www.nongnu.org/gm2/homepage.html https://www.nongnu.org/gm2/homepage.html However I doubt the language gets much use nowadays beyond some legacy code bases, its opportunity is now gone.
- kjs3 6y agofew UNIX vendors that cared to offer compiler like Sun, it was an additional acquisiation on top of UNIX SDK. The Sun C compiler was an additional cost item, just like everyone else.
- pjmlp 6y agoIndeed, so if you already had to pay for C which is a required language on any UNIX, there is no way around it, why spend the extra dollars for Ada just to feel good? That was my point.
- kjs3 6y agoBecause it's a better language for a lot of use cases? But I concede that the history of the industry indicates that "don't care" is the norm.
- johnisgood 6y agoYeah, and Ada/SPARK performs those checks people are hyped about (and more) at compile-time! Honestly, Ada does everything those languages do (regarding safety), and does more and does it better (again, talking about safety and correctness here). If you want evidence, check out my posts: https://news.ycombinator.com/item?id=19122884 https://news.ycombinator.com/item?id=19122884 (!) https://news.ycombinator.com/item?id=19245898 https://news.ycombinator.com/item?id=19245898 (!!) https://news.ycombinator.com/item?id=19274244 https://news.ycombinator.com/item?id=19274244 (!!) https://news.ycombinator.com/item?id=19274412 https://news.ycombinator.com/item?id=19274412 https://news.ycombinator.com/item?id=19770405 https://news.ycombinator.com/item?id=19770405 https://news.ycombinator.com/item?id=20776296 https://news.ycombinator.com/item?id=20776296 https://news.ycombinator.com/item?id=20934511 https://news.ycombinator.com/item?id=20934511 (!!) [3] https://news.ycombinator.com/item?id=20939336 https://news.ycombinator.com/item?id=20939336 (!!) https://news.ycombinator.com/item?id=21286061 https://news.ycombinator.com/item?id=21286061 https://news.ycombinator.com/item?id=21286292 https://news.ycombinator.com/item?id=21286292 https://news.ycombinator.com/item?id=21435869 https://news.ycombinator.com/item?id=21435869 (!) https://news.ycombinator.com/item?id=23609499 https://news.ycombinator.com/item?id=23609499 (!!)
- steveklabnik 6y agoMost of Rust's checks are at compiletime, and Ada employs runtime checks as well.
- johnisgood 6y agoIt can employ, but you do not have to (you can turn off all runtime checks and use formal verification only, something that Rust cannot do (statically verify correctness the same way you can with SPARK using GNATprove)), it can all be done at compile-time with Ada/SPARK. > These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur. > This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever occur at runtime. Specifically, GNATprove logically interprets the meaning of every instruction in the program. Using this interpretation, GNATprove generates a logical formula called a verification condition for each check that would otherwise be required by the Ada (and hence SPARK) language. Additionally, in Ada/SPARK, you can formally verify tasks (concurrency), too: https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html#preventing-data-races https://docs.adacore.com/spark2014-docs/html/ug/en/source/co.... Moreover: > SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically. Contract programming: - Ada: dynamic - SPARK: dynamic / static Run-time errors: - Ada: dynamic - SPARK: dynamic / static Data flow errors: - Ada: - - SPARK: static Strong typing: - Ada: static - SPARK: static Safer language subset: - Ada: - - SPARK: static Strict clear syntax: - Ada: static - SPARK: static Additionally, safe pointers in SPARK: https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047 https://arxiv.org/abs/1710.07047. More information about Get_Line (i.e. even where you would think you cannot go static): https://blog.adacore.com/formal-verification-of-legacy-code https://blog.adacore.com/formal-verification-of-legacy-code. [1] overflow check, index check, range check, divide by zero
- gilnaa 6y agoNot to sound too aggressive, I'm not sure why ada programmers keep being surprised at the hype. Safety (of all kinds) is not the only selling point of Rust and Zig, and the fact that Ada also have safety measures doesn't mean that it's instantly an option for me. For example, I keep seeing people hype about Zig/Rust, for all kinds of reasons; and the way that they present their arguments is very compelling. While I've heard of Ada before, AFAICT the only context in which it is brought up is to downplay hype over Rust/Zig; never as a standalone. Sounds like a PR problem, mostly. EDIT: Not to say that there aren't other problems, just saying that this point alone isn't some magic bullet. I don't like Rust because it gives me memory safety, tons of languages do that. I love Rust because the tradeoffs it gives me worth the switch, and the overall tooling and ecosystem are very well made.
- johnisgood 6y ago> I don't like Rust because it gives me memory safety, tons of languages do that. I love Rust because the tradeoffs it gives me worth the switch, and the overall tooling and ecosystem are very well made. Same applies to the tooling of Ada/SPARK, but as you have said, it is pretty much a PR issue.
- c-cube 6y agoI'm not saying it's justified, but I think the syntax is also a big impediment (just like for my daily driver, OCaml). Ada looks pretty verbose and annoying to write code in, at least if one wants to use it for side projects, small utilities, etc. rather than spaceship firmware; and that's probably how a lot of languages become popular, you need to tinker with them on small things. OCaml has seen the alternative "Reason" syntax (JS-like) grow in popularity. Maybe a C-like (or better, rust-like) syntax for Ada would help the language's adoption. People already using Ada would complain that the current syntax is fine but they're not the target demographic :-)
- ksec 6y ago> Ada looks pretty verbose and annoying to write code in, I still dont understand this, you spend 80% of the time thinking about code, 19% reading, and 1% typing.
- butterisgood 6y agoI think I'd like to get into Ada more, but I'm always a bit unsure on how to select the right toolchain (is the Dragonegg/LLVM option viable today?) etc. I would love to see something like "Rustlings" for Ada, as I found that was a good way to practice not only writing code, but reading it as well. I was able to self-teach Haskell and Erlang without any major problems, and even managed to ship applications written in it commercially.
- pjmlp 6y agoPlenty of learning paths at https://learn.adacore.com/ https://learn.adacore.com/
- butterisgood 6y agoThanks, I'll check it out! (Looks like I found a use for the new Rosetta on my M1 Mac.... I wonder when there will be builds for aarch64 for Darwin)
- AnIdiotOnTheNet 6y ago> Make something idiot-proof and the world invents a better idiot. Sure, but if you only ever give people safety scissors then you're severely limiting the kinds of things that they can build. You have to let people who know what they are doing be able to do what they need to do, so you have to be able to turn the runtime safety off. Zig can do this at the scope level.
- TchoBeer 6y agoI don't understand why there aren't any solutions like this. Why aren't there any languages with a good garbage collector but also let you turn it off and work with memory manually. Maybe there is and I don't know of it? Maybe garbage collected languages and manual memory languages require different design? I don't know.
- arc619 6y agoNim is built like this. The gc is opt-in by type and manual memory management is simple. All other types are stack allocated by default. The new gc is pretty much compiler assisted scope managed smart pointers as well. Also when using the gc you can build your own types with custom create/free/copy/move operators to do what you want without worrying about a stop the world gc. Using the arc gc pretty much compiles down to what you'd do manually. For cycles you can use the orc gc, again it's all opt in. I find this a great balance of productivity and performance, where it's easy to have high control when you want it, and still get good performance when you're not bothered.
- elcritch 6y ago+1 for Nim and being usable without a GC or for manual memory management like dealing with C apis. Though to be fair, quite a few types in the stdlib are heap based. But you can make your own static heap pool. With the new ARC & move semantics, Nim has hit a sweet spot, IMHO. It's like the language struggled to find a fit for a long time. But ARC allows very low overhead memory safety, perfect for mcu's and wasm in particular. Though perhaps Swift could be a contender in this arena as well with its ARC, but it's development is so Apple centric. What's interesting to me is that with move semantics and smarter compiler analysis, an ARC based GC overhead approaches that of Rust's compile time lifetime memory management. For any non-trivial program Rust seems to use a lot of Rc's or copies to get around lifetime analysis issues. So if the compiler can automatically figure out lifetimes in code it can eliminate many ARC operations. I hope more languages adopt more flexible ARC based gc's or improve on rusts ergonomics.
- nine_k 6y agoAda / spark may be a great thing. But how do people know? Is there a good compiler that one can install for free? Are there a few good and comprehensive books / references / guides, available online for free? If you want something to become popular, give it away. Ideally, push it. At the very least, have a limited free version. Or turn a bling eye to small-time piracy, as many vendors did for a long time. Or make it dead easy to buy it for $10. (None of the above works for you? Sorry, you have just turned down 99% of kids who might like to tinker with your tech, love it, and then promote it wherever they go. Your tech may be hot and desired in the narrow circle of pros, but it's not going to become popular and win the world.)
- nobodywasishere 6y agoThere's an Ada compiler as part of gcc. The most prominent project that i know of written in ada is ghdl.
- greatgoat420 6y agoThere was at least always the recommendation to only use the version of the Ada compiler released by the FSF as the regular GCC one is/was more encumbered.
- nobodywasishere 5y agoAre they not the same thing? https://en.wikipedia.org/wiki/GNAT https://en.wikipedia.org/wiki/GNAT
- roblabla 6y agoNot sure why you think ADA/Spark isn't free. There's GNAT[0], an open source ADA compiler that's part of the GNU toolchain, a fairly good book teaching ADA and SPARK[1] by Ada Core, and plenty of tutorials. Accessibility is really not the problem. The problem is, Ada is an old language that has many similar problems to C: lack of a good package management story, and a design by committee making language evolution glacially slow (though that also doubles as a feature). It also lacks a vibrant ecosystem like we can find in other popular languages. Furthermore, SPARK in particular takes the concept of safety much further than Rust or Zig do right now, as it allows proving the correctness of a program according to a formal specification. Rust/Zig only care about proving the absence of UB. This makes SPARK much more complex, and thus have a much higher barrier of entry. [0]: https://www.gnu.org/software/gnat/ https://www.gnu.org/software/gnat/ [1] https://learn.adacore.com/index.html https://learn.adacore.com/index.html
- 2526702934 6y ago> there's an incredibly safe and expressive language that's used in high-reliability applications like missile guidance systems, that nobody seems to talk about. Maybe because they assume that it's only used for that purpose? You talk about rocket science and you expect people to jump on the bandwagon...
- StreamBright 6y ago> Make something idiot-proof and the world invents a better idiot. :D My argument is that if I need that insane speed and safety features have to be off I should actively work for that not the other way around that I should actively work for safety. Why? Because we forget to do things. > Another language that does safety like this incredibly well is Ada (Ada/SPARK) I wanted to learn Ada for a long time. Do you have a guide or tutorial how to get into it?
- johnisgood 6y agoI once collected all of my posts about Ada which do contain lots of links that can get you started. I will not re-post them here, instead you may go to https://news.ycombinator.com/item?id=23808305 https://news.ycombinator.com/item?id=23808305. Check out the links under [2]. Especially these ones: https://news.ycombinator.com/item?id=21435869 https://news.ycombinator.com/item?id=21435869 and https://news.ycombinator.com/item?id=21437498 https://news.ycombinator.com/item?id=21437498
- StreamBright 6y agoThanks!
- johnisgood 6y agoNo problem! You might find this website useful, too, as it is filled with resources: https://www.adaic.org/learn/materials/ https://www.adaic.org/learn/materials/
- mousepilot 6y agoI loved reading about ada back in the day, how is it nowadays wrt network programming. I'm checking out gnat.sockets, does it have a snappy select() type thing like linux's epoll? Sorry if a lazy question, last time I looked at ada was decades ago and I'm surprised to find enthusiasts for it on HN. edit: an advantage for c is that you can get loads of examples just googling, sucks for less used languages I guess.
- petre 6y ago> incredibly safe […] high-reliability applications like missile guidance systems https://en.m.wikipedia.org/wiki/Cluster_(spacecraft) https://en.m.wikipedia.org/wiki/Cluster_(spacecraft)
- sigzero 6y agoYup, people are the issue.
- dapids 6y agoYes, sure, but have you actually used Ada in practice? It's not exactly ergonomic or straightforward either, it's not magic. You don't hear about the struggles of using it in practice because the projects you've pointed out are usually confidential. In my experience MISRA is a much more popular standard for secure programming in the defence industry versus Ada. MISRA is a C standard, and yes, it runs missile systems, Boeing braking systems, you name it.
- majjgepolja 6y ago> You already know someone will teach their students to always have it off because its "slower" or something. Already happening with Nim. But I'd expect a system programmer to know better. When to use release and when to use development mode. Case in point, rust doesn't catch integer overflows in release build either. Maybe Efficiency is more important than we think?