Mastodawn

mcc May 17, 2025

#BabelOfCode 2024
Week 9
Language: Ada (Spark?)

Confidence level: High

PREV WEEK: https://mastodon.social/@mcc/114463342416949024
NEXT WEEK: https://mastodon.social/@mcc/114582208242623432

So I start reading the manual for Ada. I think: This is *great!* This has all these features, conveniences etc I was wishing for for years in C++, and didn't get until I jumped to Rust. I might have been using this for games in 2010 if I'd dug into it then!

Then I start writing an actual Ada program. It turns out to be basically a pain in the ass.

Now, it's possible that the reason I'm unhappy is I jumped directly into something Ada is not designed for. However, that thing I jumped into was "load a file at runtime into a string whose length is not known at compile time". I don't think this should be so hard in a recently-revised language. (I seem to be tragically consistent in this challenge at accidentally picking languages whose input systems prefer structured data-- like Ada and Fortran-- on puzzles where I'm parsing raw ASCII art.)

mcc May 17, 2025

To pick at this. "Software" can mean a do of different things! There's environments where you spend lots of time poking at text strings— text files in a world where the UNIX "everything is a file" philosophy won, webdev. There's really important environments where they don't! If you're writing backend software interacting with databases and network services, maybe it turns out Ada is *perfect* for this environment and you don't care about the friction on files and variable-length strings. Dunno.

mcc May 17, 2025

Anyway. I was able to open a file whose name is given on the command line, but not read lines from it (the line reader only wants to work with stdin). I was not able to take an arbitrary-length string from stdin (I hardcoded to 10,000 bytes, the length of my largest input). I wasted a bunch of time on it, decided this wasn't important, and moved on. I'm trying to write "professional" software in this challenge and Ada, at least for the UNIX-y cmdline-and-files environment, did not reward that.

mcc May 17, 2025

Compromises on basic things continue. I want to create an array whose size is not known at compile time. I believe I can declare this with

Mem : Array (Natural range <>) of Integer range -1..Integer'Last;

But this errors there's no initialization. You can initialize an array to a fixed value with (Others => -1), but then it doesn't know the size. I wind up making a sub-procedure *just* because that is the only syntax I can find for initializing an array to a size. https://github.com/mcclure/aoc2024/blob/b46079ddcb5c45d52af5882e940a593050c7beb9/09-01-disk/src/puzzle.adb#L14

aoc2024/09-01-disk/src/puzzle.adb at b46079ddcb5c45d52af5882e940a593050c7beb9 · mcclure/aoc2024

Advent of Code 2024 challenge (laid-back/"babel" version) - mcclure/aoc2024

GitHub

mcc May 17, 2025

Small observations:

- Inner procedures and functions of a larger procedure and function can access the outer procedure's local variables. That's nice. I suspect this is hiding some sort of horrible restriction on recursion, but it's nice.

- The error messages, at least in "gnat" the open source Ada compiler, are NOT good. I think this is downstream from the language having lots of minor similar-but-distinct concepts instead of single powerful concepts. There's a lot of jargon and lots of edges

mcc May 17, 2025

Something I don't know how you'll feel about: You know how in every programming language except Lua you index arrays from 0, and in Lua you index arrays from 1? In Ada, if I'm understanding this correctly, you choose whether your code indexes arrays from 0 or 1. *On an array by array basis*. You could mix 0- and 1-indexed arrays in the same code. You could have an array which contains 10 elements at indexes 10 through 19 inclusive, if you wanted. An array is a map with integer keys in a range

…

mcc May 17, 2025

Man writing Ada is *really* making me think I was too hard on Haskell

mcc May 17, 2025

Maybe the problem with Ada was that the things it was trying to do were too advanced for the tools that were available to the designers at the time.

I'm having an awful problem with a very straightforward bit of code because I want to scan over some code iterating a variable erratically. But I don't have any good value to give *before iteration begins*— because Ada integer types are range-limited, I can't use "0". This would be no problem at all I had Option<>. But I don't have Option<>.

mcc May 18, 2025

Guh. Part 1 done. It was ok once I actually had my data loaded into memory, but every moment up until there was pulling teeth, and honestly the ergonomics weren't *great* after that. The final insult was it taking a startling amount of time trying to figure out how to convert an Integer to a Long_Integer when it turned out my result was over 32 bits. It's Long_Integer(), but StackOverflow was a bunch of "how do I cast in Ada?" "*bragging* In Ada, you don't NEED to cast!"

https://github.com/mcclure/aoc2024/blob/9048d0cd5d29fc8f987c4f7369360279199fc2b0/09-01-disk/src/puzzle.adb

aoc2024/09-01-disk/src/puzzle.adb at 9048d0cd5d29fc8f987c4f7369360279199fc2b0 · mcclure/aoc2024

Advent of Code 2024 challenge (laid-back/"babel" version) - mcclure/aoc2024

GitHub

mcc May 18, 2025

I pushed through Part 2 just to get it over with. I could have done a very clean, efficient implementation in any other language, but Ada makes creating new arrays enough of a pain I just wound up like… doing it the dumb nested loops way. Whatever. I realized in literally the final line of code I wrote that part of why I was struggling with loops was I didn't know "exit" existed.

It works. It's even relatively efficient. I don't feel proud of this code.

https://github.com/mcclure/aoc2024/blob/3adbb87169b82453caafd75308837c203247edc4/09-02-disk/src/puzzle.adb#L80

aoc2024/09-02-disk/src/puzzle.adb at 3adbb87169b82453caafd75308837c203247edc4 · mcclure/aoc2024

Advent of Code 2024 challenge (laid-back/"babel" version) - mcclure/aoc2024

GitHub

mcc May 18, 2025

There's a lot I'm curious about in Ada. I'd really like to know more about its builtin Task primitive. I find the basic "in the small" writing of Ada frictionful enough I have lost my curiosity about attempting to experience its high-level primitives. I was originally intending to do part 1 of this puzzle in Ada and part 2 in Spark, but I don't… I just kinda want to stop. This puzzle has taken very almost the whole week, and part of that is WestJet's fault (long story), but I want to move on.

mcc May 18, 2025

A problem I anticipated with this "Babel of Code" project and sure am hitting now: The AOC puzzles are a great way to learn a language, but they'll always focus on *only part* of a language. When I hit smalltalk, I'll have little opportunity to use objects. Multiprocessing, or verification capabilities like Spark, can be applied in *some* puzzles, but it's hard to know *which* puzzles until it's half complete. Like, what formal properties does THIS puzzle have to verify?

https://adventofcode.com/2024/day/9

Day 9 - Advent of Code 2024

mcc May 18, 2025

#BabelOfCode 2024
Week 9.5??
Language: Spark

Against my better judgement, but since it was one of the main things that intrigued me about Ada, I decide to port my "day 9" solution to Spark.

I put at the top of my program:

with SPARK_Mode => On

And run it. Nothing happens. Or rather it runs normally. I assume that this sets an attribute read by the Spark toolchain, and is ignored by basic Ada.

The docs suggest running gnatprove. Which… isn't in debian apt? I think I have to go to Github?

mcc May 18, 2025

gnatprove-x86_64-linux-14.1.0-1.tar.gz turns out to be 412MB gzipped, and contains both a complete installation of GCC and a Python 3. That seems like why dpkg exists, but it seems the AdaCore corporation really, really wants me to be using gnatprove as part of their IDE. Which I guess is also why gnatprove unlike gnat itself can't be run on single files and I have to make a project file. Whatever, fine.

It's running. It gives me hundreds of validation errors. Which I guess is what I wanted.

mcc May 18, 2025

Spark is immediately proving itself interesting. My very first error:

puzzle.adb:47:21: medium: range check might fail, cannot prove upper bound for 1
47 | Mem_Idx := 1;
| ^ here
reason for check: value must fit in the target type of the assignment

What this means: Mem_Idx has type
Mem_Idx : Natural range 1..Mem_Len;
where Mem_Len is a Natural argument of the procedure. But *nothing guarantees Mem_Len is nonzero*. That's a real uninterrogated assumption!

mcc May 18, 2025

More odd friction. It turns out Ada/Spark don't allow integer narrowing on a argument parameter. Why? They just don't. OK, so I create a typedef Nonzero for the integer range of Mem_Len. Now anytime I say I have a Natural of range 1…Mem_Len, it complains I used Natural and not Nonzero. Bro!! Bro u r introducing an unnecessarily strong binding between structural and nominal typing!! It could have detected Natural range 1..Mem_Len necessarily conforms to Nonzero, but instead I have to annotate it.

mcc May 18, 2025

Continuing with the "couldn't you do the math yourself?" complaints, it now turns out I can't add Natural (range 0..Natural'Last) to Nonzero (range 1…Natural'Last). These types share a common upper bound and neither may be zero; this addition is safe in all cases!

I guess I expected working with a theorem prover language would have lots of paperwork. I don't know if I expected this. (Also *this* issue is Ada not Spark?) Would Idris have been able to figure this one out? I bet Prolog would have.

mcc May 18, 2025

Okay I guesss I got frustrated too early. It turns out that I can avoid all this nominal typing paperwork by, instead of attempting to refine the value of Mem_Len by its parameter type, refining it by *contract*. I add a contract that Mem_Len > 0 and Spark no longer complains about assignments. That's entirely fine. It would have been nice if Ada had been more helpful, but the point is whether Spark offers capabilities to keep the friction/frustration levels beneath the ragequit point. Fiiine

mcc May 18, 2025

I realize I'm focusing on entry-level nitpicks here, but I do notice this is not the first time I've run into a frustrating limitation in some construct of Ada only to discover I can avert the limitation by using a different, similar construct. It speaks to an actual problem with Ada/Spark: There is too much syntax. I believe that Ada was designed around readability to the point it harms writeability (and doesn't help readability as much as it should, as the eyes glaze at all this boilerplate).

DesChips May 19, 2025

@mcc are you ok for some insight from an Ada/SPARK dev?

mcc May 19, 2025

@DesChips I'd be curious yes. However if you were about to explain the type/subtype distinction to me, I have received that help already in the time since my post: https://mastodon.social/@mcc/114535020019461764

Thanks

DesChips May 20, 2025

@mcc Sub-types are indeed important ^^ What I noticed first is that you use anonymous subtypes and constraints a lot, where I would define explicit types. For example, with the array of integers:

type Mem_Length is range 0 .. 20_000;

type Any_Mem_Element is new Integer range -1 .. Integer'Last;
Invalid : constant Any_Mem_Element := -1;
subtype Valid_Mem_Element is Any_Mem_Element range 0 .. Any_Mem_Element'Last;

type Mem_Array is array (Mem_Length range <>) of Any_Mem_Element;

Jordan May 18, 2025

@mcc If this is a fixed-width type, you could overflow, right?

Paul Khuong May 18, 2025

@jrose @mcc or otherwise exceed the bounds.

mcc May 18, 2025

@jrose That is an unrelated problem. (And one that Ada/Spark overall seem worryingly unconcerned with. If I understand the docs right, it only checks for type overflow *when the expression is assigned*? So if you say z := (a + x) * y and (a+x) int-overflows to 2, and 2*y is within the type range, that passes the runtime checks despite being wrong arithmetic. That's disturbing enough I honestly *hope* I am reading the docs wrong.)

mcc May 18, 2025

@jrose if I'm *not* reading the docs wrong, then I interpret this as downstream from Ada trying to introduce guardrails for program correctness in an era before coders had really developed best practices for correctness. (Or at least before security vulnerability authors got really good.)

Robin Leroy May 18, 2025

@mcc @jrose You are reading the docs wrong, see AARM 4.5(10) http://www.ada-auth.org/standards/2yaarm/html/AA-4-5.html#p10 and 3.5.4(24) http://www.ada-auth.org/standards/2yaarm/html/AA-3-5-4.html#p24.

What this is saying is that the implementation could compute the sum a + x in a type wider than that of a and x, where that sum does not overflow.

Operators and Expression Evaluation

mcc May 18, 2025

@eggrobin @jrose Thanks

EndlessMason May 18, 2025

@mcc Isn't Natural'Last + 1 out of the range tho?

mcc May 18, 2025

@EndlessMason If that were a problem then there would be a type error on adding two Naturals.

EndlessMason May 18, 2025

@mcc I'm not great at type math, but I try.

mcc May 18, 2025

@EndlessMason I mean, put a different way, that is a real issue, but it is an issue of a kind the language doesn't actually check for.

Robin Leroy May 19, 2025

@mcc I guess you figured it out by now, but the issue here is confusion between types and subtypes; the point of defining a new type (type T is range blah, or type T is new U [range blah];), besides allowing for different representations, is to disallow mixing them (as noted above, here I think it makes sense to have two types).

To describe constrained values, use a subtype (subtype T is U range blah;). The type Integer has subtypes Natural (0 .. Integer'Last) and Positive (1 .. Integer'Last).

mcc May 19, 2025

@eggrobin Hi, sorry… are you saying that

`type Nonzero is new Natural range 1..Natural'Last;`

is introducing the hard "no mixing!" nominal type, whereas

`subtype Nonzero is new Natural range 1..Natural'Last;`

is just like creating a shorthand expansion for `Natural range 1..whatever`, and would have evaded my error above?

Robin Leroy May 19, 2025

@mcc Exactly (well, no `new` in the subtype declaration).

Also, that subtype Nonzero has a name already, it is called Positive, RM A.1(13) http://www.ada-auth.org/standards/2yaarm/html/AA-A-1.html#p13.
It is used very often, e.g.,
type String is array (Positive range <>) of Character
http://www.ada-auth.org/standards/2yaarm/html/AA-A-1.html#p37.

Also note that since Ada 2012, you can have subtypes that are fancier than ranges with Static_Predicate, see the example in RM 3.2.4(40) http://www.ada-auth.org/standards/2yaarm/html/AA-3-2-4.html#p40.

The Package Standard

Robin Leroy May 19, 2025

@mcc Re
> creating a shorthand expansion for `Natural range 1..whatever`

Note that Ada has renaming declarations for most things, RM 8.5 http://www.ada-auth.org/standards/2yaarm/html/AA-8-5.html#, but not types.

The reason is that you can rename a type by writing subtype T is U, as pointed out in 8.5(6).

Renaming Declarations

lambdageek May 18, 2025

@mcc are you planning to try LiquidHaskell?

mcc May 18, 2025

@lambdageek I'm going to try Idris… I was thinking of doing another Haskell week to try Linear Haskell (which I think is just GHC with a flag) would Liquid Haskell layer atop that happily?

@mcc Gonna nerd-snipe you with F* 😉

https://fstar-lang.org/

"is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving."

E.g. proving function equivalence:
https://floss.social/@janriemer/114446026791565094

Crazy language! 😄

F*: A Proof-Oriented Programming Language

mcc May 18, 2025

@janriemer @lambdageek Hm. And it runs on the CLR? Is it a subset/superset of F#?

@mcc @lambdageek
It compiles to OCaml by default, but can also compile to F#, C and even WASM (using a tool called KaRaMeL 😋 https://github.com/FStarLang/karamel)!

GitHub - FStarLang/karamel: KaRaMeL is a tool for extracting low-level F* programs to readable C code

KaRaMeL is a tool for extracting low-level F* programs to readable C code - FStarLang/karamel

GitHub

lambdageek May 18, 2025

@mcc I'm not sure.

https://github.com/ucsd-progsys/liquidhaskell/issues/1887

it looks like maybe it will work.

although I don't know if there's any meaningful interaction between the linear and refinement types

LiquidHaskell binary does not work with LinearTypes · Issue #1887 · ucsd-progsys/liquidhaskell

Running the binary for liquidhaskell-0.8.10.2 on any file containing a pragma for the LinearTypes language extension returns this: » liquid <File>.hs liquid: Unsupported extension: LinearTypes Is t...

GitHub

Robin Leroy May 19, 2025

@mcc The thread made me mildly curious, so I took a stab at it.

Caveat, while I am on WG 9 and an observer on the Ada Rapporteur Group, I am there only as a liaison from Unicode; I have only written Ada recreationally, and not much of it at that. My father used to chair the ARG and work on Ada compilers; most of what I know is from him.

https://github.com/eggrobin/ada-playground/blob/master/src/ada_playground.2.ada

ada-playground/src/ada_playground.2.ada at master · eggrobin/ada-playground

Contribute to eggrobin/ada-playground development by creating an account on GitHub.

GitHub

Robin Leroy May 19, 2025

@mcc One thing where Ada shines that is relevant here is the ease with which you can define lots of integer types and subtypes and use them just like the predefined ones.

In this case, there are clearly two kinds of integers, and mixing those up is a bug—except in the weird checksum, where you needed a conversion anyway—: the block indices (and file sizes in blocks), and the file indices.

Robin Leroy May 19, 2025

@mcc In my code at least, I rely on the file sizes being nonzero; this gets checked when reading the input just by introducing this subtype here, never mentioned again: https://github.com/eggrobin/ada-playground/blob/39ea262b9e581f88fd7aa5b9baf528ef1f6e1ace/src/ada_playground.2.ada#L11-L14.

On the runtime-sized array thing, I am recursing and returning a slice here: https://github.com/eggrobin/ada-playground/blob/39ea262b9e581f88fd7aa5b9baf528ef1f6e1ace/src/ada_playground.2.ada#L40-L63.

I think gnat has a “secondary stack” that lives on the heap, but some implementations for heap-averse applications returned those on the stack (with the caller not popping while the result is needed).

ada-playground/src/ada_playground.2.ada at 39ea262b9e581f88fd7aa5b9baf528ef1f6e1ace · eggrobin/ada-playground

Contribute to eggrobin/ada-playground development by creating an account on GitHub.

GitHub

Robin Leroy May 19, 2025

@mcc Of course if I were writing this “for real” I would probably just use a Vector (still indexed on File_ID, the package is generic on both Index_Type and Element_Type) instead of recursively doubling arrays; the container libraries have been around for twenty years now.

Robin Leroy May 19, 2025

@mcc I have never tried SPARK; but looking at the issues you were running into there, I wonder if things might be a bit smoother if you were more aggressively typing things to start with, instead of doing it all with subtypes of Standard.Integer.

Dr David Mills May 17, 2025

@mcc I've never used Ada, but I wrote VHDL professionally for a year or so 23 years ago. I really got it then. I've not looked at it since.

mcc May 17, 2025

@dtl I read the VHDL spec once, and it made a lot of sense. But also the Ada spec made a lot of sense when I read it, and when I tried to actually write it I liked it less.

none gender with left politics May 17, 2025

@mcc I have this mug that I got from when my dad was working as a SWE in the 70s. I've never written Ada or I imagine I might have to cross out the heart.

Shiny Quagsire May 18, 2025

@vikxin @mcc tbh I have coworkers who would get a kick out of this mug lol

mcc May 18, 2025

@ShinyQuagsire @vikxin I have a friend named Ada and I want to buy this mug for her wife

none gender with left politics May 18, 2025

@mcc @ShinyQuagsire Unfortunately the other side is branded with a company that hasn't existed in a long time. I don't think they sell them anymore.

blueorangeblue May 17, 2025

@mcc the best of both worlds!

✧✦Catherine✦✧May 17, 2025

@mcc inner procedures (in gnat) require executable stack because creating a closure puts a trampoline on stack so that you would not need "fat pointers" like Rust does

this is also why you can't compile GHDL to WebAssembly

mcc May 17, 2025

@whitequark *strangled noise*

✧✦Catherine✦✧May 17, 2025

@mcc it's a part of the ABI now! i think this is like, the overwhelming cause for executable stacks today

vriska, thief of light

@whitequark @mcc i think ghdl might no longer rely on this? nixpkgs' ghdl doesn't have any rwx mappings

✧✦Catherine✦✧May 17, 2025

@leo @mcc oh that's exciting, i should revisit it

Brooks Davis May 17, 2025

@whitequark @leo @mcc I know AdaCore did a CHERI port and at least at the moment we enforce W^X in CheriABI

✧✦Catherine✦✧May 17, 2025

@brooks @leo @mcc I faintly recall that it's only using W+X on X86 in first place due to historical reasons, it might've never been that way on ARM in first place