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

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

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

…

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<>.

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

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

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

#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?

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.

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!

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.