Top all-time · #555
AdaCore
Company blog · blog.adacore.comprogrammingsecurity
AdaCore is the company blog at blog.adacore.com, writing about programming and security. Since 2015, 106 different Hacker News readers have linked it 277 times, most often “Pointers in SPARK/Ada inspired by Rust ownership model”. It is still writing: the last post was on 2026-10-30, and you can follow it by feed.
AdaCore is the leading provider of commercial software solutions for Ada, C and C++ — helping developers build safe and secure software that matters.
Most-linked posts?
- Pointers in SPARK/Ada inspired by Rust ownership model17 people · 24 mentions · first linked 2019-06-06
- Should I choose Ada, SPARK, or Rust over C/C++? (2024)6 people · 7 mentions · first linked 2024-09-27
- I can’t believe that I can prove that it can sort5 people · 6 mentions · first linked 2022-07-01
- CuBit: A General-Purpose Operating System in SPARK/ Ada (2020)5 people · 5 mentions · first linked 2020-06-10
- Ada 202x Support in Gnat5 people · 5 mentions · first linked 2020-10-29
- Proof of code with pointers now possible in SPARK using pledges4 people · 5 mentions · first linked 2019-10-09
- /a-modern-syntax-for-ada4 people · 4 mentions · first linked 2020-09-03
- Going Beyond Ada 20224 people · 4 mentions · first linked 2021-06-03
- A New Era for Ada/Spark Open Source Community4 people · 4 mentions · first linked 2022-06-02
- From Ada to Platinum Spark: A Case Study for Reusable Bounded Stacks4 people · 4 mentions · first linked 2020-05-15
What Hacker News says?
I use it to learn new languages - this year it's Ada - https://blog.adacore.com/announcing-advent-of-ada-2024-codin...
Comment linking /announcing-advent-of-ada-2024-coding-for-a-cause
on “Advent of Code 2024”Submitted AdaCore and Ferrous Systems Joining Forces to Support Rust as a story · 357 points
HN discussionAda has built-in C/C++ interfacing: https://gcc.gnu.org/onlinedocs/gnat_ugn/Interfacing-to-C.htm... For instanced I used it here to write Ada programs for the C API of the Pebble smartwatch: https://blog.adacore.com/make-with-ada-formal-proof-on-my-wr...
Comment linking /make-with-ada-formal-proof-on-my-wrist
on “Ask HN: Best way to learn modern C++?”Submitted Nvidia Security Team: “What if we just stopped using C?” (2022) as a story · 306 points
HN discussion> Ada should be considered dead because it doesn't have an npm full of super[1] useful[2] libraries? Wait! There is Alire [1][2]! There is a list of "crates", you can easily include them into your project, and so forth. This is pretty much the same as https://crates.io or https://pkg.go.dev , which means people really should throw their misconceptions away and actually do some research before concluding that the lan…
Comment linking /first-beta-release-of-alire-the-package-manager-for-ada-spark
on “Linux Rust Support”Submitted I can’t believe that I can prove that it can sort as a story · 270 points
HN discussionThat said, I still use valgrind because we have to integrate C libraries sometimes (libpcl is my favorite culprit, only because I'm trying , and there's still possibility to blow the stack (yeah you can use gnatstack to get a good idea of your maximum stack size, but it's doesn't cover the whole Ada featureset and stack canaries - fstack-check don't catch everything. edit Also massif, call/cachegrind and hellgrind h…
Comment linking /running-american-fuzzy-lop-on-your-ada-code
on “Twenty years of Valgrind”Submitted Nvidia Security Team: “What if we just stopped using C?” as a story · 257 points
HN discussionDepends on which dynamic memory you are talking about. Ada can manage dynamic stacks, strings and arrays on its own. For example, Ada has what one could call type safe VLAs, instead of corrupting the stack like C, you get an exception and can redo the call with a smaller size, for example. As for explicit heap types and Ada.Unchecked_Deallocation , yes if we are speaking about Ada 83. Ada 95 introduced controlled ty…
Comment linking /header-storage-pools
on “Twenty years of Valgrind”Submitted Introduction to Ada: a project-based exploration with rosettas as a story · 194 points
HN discussion> It’s truly the only low-level language that could actually be used for systems programming. No it is not. There is Ada/SPARK and has been for a long time, and it is for critical systems. I recommend checking out https://blog.adacore.com/ for examples, there is plenty of that. For one: "An Embedded USB Device stack in Ada". There are also many articles about SPARK. For example: "Enhancing the Security of a TCP Stac…
Comment linking /
on “Rust support in the Linux kernel”Submitted There's a mini RTOS in my language as a story · 159 points
HN discussion>> I don't know Ada well personally >> But I'm not very educated. If you don't know, please don't speculate. I use Ada professionally and I am experimenting with Rust. Rust has great promise and I am interested to see where it will go, especially as an alternative to C++. >> it's a bit less advanced than Rust at static checks Ada 2012 has comparable and in many cases more advanced static checks than Rust with the ex…
Comment linking /using-pointers-in-spark
on “Swift System Is Now Open Source”Submitted Going Beyond Ada 2022 as a story · 123 points
HN discussion> all languages that target LLVM (including C, C++, Fortran, Ada, Julia, Swift and others) can be used in WebAssembly. Having LLVM doesn't mean that webassembly Just Works, in the same way that having LLVM doesn't mean that all of its architectures Just Work. And even after getting past the "hello world" stage, there's a lot of other work to do to make it more than just a toy. Let's take Ada, for example. https://bl…
Comment linking /use-of-gnat-llvm-to-translate-ada-applications-to-webassembly
on “Moving from TypeScript to Rust / WebAssembly”Submitted Should I choose Ada, SPARK, or Rust over C/C++? (2024) as a story · 111 points
HN discussion> You can prove in math your design will work It's possible, but extremely labour-intensive, to mathematically prove the correctness of a program. I mentioned this in my previous comment. > In Programming, unless you are working at switch levels, how could you prove your code is most optimized? 'Most optimised' is an entirely different problem than 'your design will work'. Complexity theory lets us do something like…
Comment linking /tokeneer-fully-verifed-with-spark-2014
on “Foundations of Software Engineering”Submitted Ada crate of the year 2024 announced as a story · 106 points
HN discussionOr in Ada. Ada 202x[1] brings enhancements like the parallel block, making parallelism easier to express, somewhat similar to Rust's approach but still with Ada's emphasis on clarity and safety. [1] https://blog.adacore.com/ada-202x-support-in-gnat (2020) There may be more enhancements that I may not know about or remember, although I did mention Ada's constructs for safe concurrent code before.
Comment linking /ada-202x-support-in-gnat
on “I Created 175 Fonts Using Rust”Submitted Ten Years of Using SPARK to Build CubeSat Nano Satellites with Students as a story · 91 points
HN discussionThink of them as richer versions of asserts. And in languages where they are first-class parts of the language, that is they become meaningful metadata on functions, variables, classes, etc., then you can end up deriving tests from them or running them through a prover (not always possible, or might restrict you to a subset of the language). They are complementary to the type system and test systems, just like asser…
Comment linking /i-cant-believe-that-i-can-prove-that-it-can-sort
on “Six programming languages I’d like to see”Submitted First beta release of Alire, the package manager for Ada/SPARK as a story · 86 points
HN discussionWant to make a fast application on a pebble and with actual type checking? C and Ada won't complain or blur your lines... http://blog.adacore.com/make-with-ada-formal-proof-on-my-wri...
Comment linking /make-with-ada-formal-proof-on-my-wrist
on “Rust and the Future of Systems Programming [video]”Submitted From Rust to Spark: Formally Proven Bip-Buffers as a story · 84 points
HN discussionhttps://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo... > Standard Ada supports safe use of pointers (“access types” in Ada) via strongtype checking, but safety is guaranteed only for programs where there is no explicit deallocation of pointed-to objects This validates "With Ada you can't use dynamic memory allocation and pointers safely, unless you buy into SPARK". (GC not relevant in this context.) > In th…
Comment linking /using-pointers-in-spark
on “Linux kernel in-tree Rust support”Submitted Proving the Correctness of GNAT Light Runtime as a story · 75 points
HN discussionI am inclined to agree. By the way: when I first read about Rust and its "safety features" that make it appealing to people, the first programming language that came to mind was Ada. I suppose it lacks the hype (and consequently a vibrant ecosystem, IMO) and people hold absurd misconceptions of the language[1]. :/ I am trying my best to dissipate those misconceptions on Hacker News; hopefully it does not count as sh…
Comment linking /gnat-community-2020-is-here
on “Linux kernel in-tree Rust support”Submitted Ada on any ARM Cortex-M device, in just a couple minutes as a story · 73 points
HN discussionYou can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"): https://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4 You can similarly express ghost properties of your types, even though we don't have ghost fields in SPARK. For more on ghost code in SPARK, you can look at this presentation last year from my c…
Comment linking /tetris-in-spark-on-arm-cortex-m4
on “Implications of Rewriting a Browser Component in Rust”Submitted Ada on FPGAs with PicoRV32 as a story · 73 points
HN discussion
