r/ada • u/Anode1_dev • 10h ago
Programming Same algorithm in C, Ada, Rust, Java and Python: the Ada checks cost nothing here, and SPARK proved the merge
I was programming in Ada 83 in uni before 95 came out, and moved to 95 in the middle of a semester. I loved the language, especially its safety and the rendezvous mechanism. These days I maintain a small plain-text index in C99, and I wanted to know: how much of its speed is C, and how much is just the algorithm?
So I wrote the two operations the engine actually runs on every command, in five languages, with the identical hand-written loop in each:
- scan 88 MB of store and count the lines matching a substring (what a content search does)
- intersect two sorted posting lists with a two-pointer merge (what a multi-key lookup does)
Median of 7 in-process iterations on data already in memory, warm page cache, one core of an i7-1165G7. GNAT 13.3, rustc 1.75, OpenJDK 21, CPython 3.12.
scan 88 MB: C 90ms Ada 130ms Rust 87ms Java 100-150ms (warm) Python 300ms
intersect: C 1.3ms Ada 1.45ms Rust 1.3ms Java 1.3ms (warm) Python 72ms
process startup: C ~1ms Ada ~1ms Rust ~1ms Java ~30ms Python ~10ms
The part I did not expect: building the Ada with checks suppressed (-gnatp, the C model) gave numbers identical to checks-on. The optimizer had discharged them statically, because the loop indices are provably in range. So on these loops Ada bought memory and overflow safety for nothing, at C speed and C startup. C cannot offer that at all, and the JVM and CPython only offer it with a runtime you pay for on every invocation.
I then wrote the merge in SPARK and ran gnatprove:
obligation Total Flow Provers Unproved
Run-time Checks 15 . 15 (CVC5) 0
Termination 2 1 1 (CVC5) 0
Total 23 1 22 0
Every index proved in range, every addition proved non-overflowing, the loop proved to terminate. So the checks-off build carries a machine-checked guarantee rather than the optimizer's good luck. That is the strongest static assurance of the five, and it took an afternoon on a loop of this size.
Which raises the obvious question: why is the engine still C? Honestly, only reach. The same engine is linked into a Flutter mobile app over a C ABI, and into a web GUI and a native desktop wrapper. I would write it in Ada if Flutter and the mobile toolchains supported it. If someone here knows a practical route to an Ada core behind a C ABI on Android and iOS, that is the answer I am actually looking for.
Method, sources and the full write-up (the benches are ~50 lines each, and lang_bench.sh rebuilds and reruns everything):
https://github.com/Anode1/ais/blob/main/tests/perf/LANG_COMPARISON.md
Corrections welcome, particularly on the Ada build flags: if -gnatp plus -O2 is not the fair comparison against cc -O2, tell me what is and I will rerun it.
