#BabelOfCode 2024
Week 9
Language: Ada (Spark?)
Confidence level: High
PREV WEEK: mastodon.social/@mcc/114463342…
NEXT WEEK: mastodon.social/@mcc/114582208…
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.
#BabelOfCode 2024
Week 8
Language: FennelConfidence level: High
PREV WEEK: mastodon.social/@mcc/114433465…
NEXT WEEK: mastodon.social/@mcc/114463342…
RULES: mastodon.social/@mcc/113676228…Lua is my favorite programming language. Because of Reasons¹ I have stopped using it, but it is still a jewel of design to me. Any description of what I want in a programming language will sound like "Lua, but—"
Fennel is "Lua, but with LISP syntax". Which is… if anything the opposite of what I want. Hm.
¹ I NEED TYPES
mcc (@mcc@mastodon.social)
#BabelOfCode 2024 Week 8 Language: Fennel Confidence level: High PREV WEEK: https://mastodon.social/@mcc/114433465965880352 NEXT WEEK: https://mastodon.social/@mcc/114463342416949024 RULES: https://mastodon.Mastodon
mcc
in reply to mcc • • •mcc
in reply to mcc • • •mcc
in reply to mcc • • •mcc
in reply to mcc • • •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. github.com/mcclure/aoc2024/blo…
aoc2024/09-01-disk/src/puzzle.adb at b46079ddcb5c45d52af5882e940a593050c7beb9 · mcclure/aoc2024
GitHubmcc
in reply to mcc • • •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
✧✦Catherine✦✧
in reply to 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
reshared this
mcc e Oblomov reshared this.
mcc
in reply to ✧✦Catherine✦✧ • • •✧✦Catherine✦✧
in reply to mcc • • •mcc
in reply to mcc • • •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
…
blueorangeblue
in reply to mcc • • •mcc
in reply to mcc • • •Oblomov reshared this.
Dr David Mills
in reply to mcc • • •mcc
in reply to Dr David Mills • • •mcc
in reply to mcc • • •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
in reply to mcc • • •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!"
github.com/mcclure/aoc2024/blo…
aoc2024/09-01-disk/src/puzzle.adb at 9048d0cd5d29fc8f987c4f7369360279199fc2b0 · mcclure/aoc2024
GitHubmcc
in reply to mcc • • •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.
github.com/mcclure/aoc2024/blo…
aoc2024/09-02-disk/src/puzzle.adb at 3adbb87169b82453caafd75308837c203247edc4 · mcclure/aoc2024
GitHubmcc
in reply to mcc • • •mcc
in reply to mcc • • •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?
adventofcode.com/2024/day/9
Day 9 - Advent of Code 2024
adventofcode.comOblomov reshared this.
mcc
in reply to mcc • • •#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
in reply to mcc • • •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
in reply to mcc • • •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
in reply to mcc • • •lambdageek
in reply to mcc • • •mcc
in reply to lambdageek • • •Jan
in reply to mcc • • •Gonna nerd-snipe you with F* 😉
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:
floss.social/@janriemer/114446…
Crazy language! 😄
@lambdageek
Jan :rust: :ferris: (@janriemer@floss.social)
FLOSS.socialmcc
in reply to Jan • • •Jan
in reply to mcc • • •It compiles to OCaml by default, but can also compile to F#, C and even WASM (using a tool called KaRaMeL 😋 github.com/FStarLang/karamel)!
GitHub - FStarLang/karamel: KaRaMeL is a tool for extracting low-level F* programs to readable C code
GitHublambdageek
in reply to mcc • • •I'm not sure.
github.com/ucsd-progsys/liquid…
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
GitHubmcc
in reply to mcc • • •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
in reply to mcc • • •mcc
in reply to mcc • • •DesChips
in reply to mcc • • •mcc
in reply to DesChips • • •@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: mastodon.social/@mcc/114535020…
Thanks
mcc
2025-05-19 14:41:50
DesChips
in reply to 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;
DesChips
in reply to DesChips • • •Then you can declare your array like so:
Mem_Len : constant Mem_Length := 42;
Memory : Mem_array (1 .. Mem_Len) := (others => Invalid);
You can also check for valid elements, e.g.:
for Elt of Memory loop
if Elt in Valid_Mem_Element then
--- something
end if;
end loop;
DesChips
in reply to DesChips • • •arclight
in reply to DesChips • • •@DesChips This is fascinating! I'm confused by the '(others => Invalid)' value being assigned to Memory in the line
Memory : Mem_array (1 .. Mem_Len) := (others => Invalid);
Mem_Len (set to 42) is limited to the range 0 .. 20000. In the assignment of (others => Invalid), what are the 42 elements of Memory assigned to -- Invalid? Or something else (or undefined, which seems very anti-Ada)? Or is Invalid returned if Memory is accessed with an index outside 1 .. 42, i.e. 0, 43 .. 20000?
I guess I'm mostly confused by what 'others' refers to.
DesChips
in reply to arclight • • •@arclight When "others" is alone in the array literal (aggregate) it means all the elements of the array. Which, in this case, I set to the value of the "Invalid" constant. The word "others" makes more sense when you provide values from some elements of the array and a default value for all other elements, e.g.:
Memory : Mem_array (1 .. Mem_Len) := (1 => 2, 4 => 0, 16 => 13, others => Invalid);
learn.adacore.com/courses/intr…
“learn.adacore.com"
learn.adacore.commcc
in reply to DesChips • • •DesChips
in reply to mcc • • •@arclight
It's just a constant declared to be the value -1 (matching what you have in the code screenshots in this thread). It's an actual byte value that you can store in a variable of type Any_Mem_Element.
A : Any_Mem_Element := Invalid.
and then I excluded this value from the Valid_Mem_Element subtype by defining the range from 0 to last:
subtype Valid_Mem_Element is Any_Mem_Element range 0 .. Any_Mem_Element'Last;
Jordan
in reply to mcc • • •mcc
in reply to Jordan • • •mcc reshared this.
mcc
in reply to mcc • • •Robin Leroy
in reply to mcc • • •You are reading the docs wrong, see AARM 4.5(10) ada-auth.org/standards/2yaarm/… and 3.5.4(24) ada-auth.org/standards/2yaarm/….
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
www.ada-auth.orgmcc reshared this.
mcc
in reply to Robin Leroy • • •EndlessMason
in reply to mcc • • •mcc
in reply to EndlessMason • • •EndlessMason
in reply to mcc • • •mcc
in reply to EndlessMason • • •Robin Leroy
in reply to 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
in reply to Robin Leroy • • •@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
in reply to 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) ada-auth.org/standards/2yaarm/….
It is used very often, e.g.,
type String is array (Positive range <>) of Character
ada-auth.org/standards/2yaarm/….
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) ada-auth.org/standards/2yaarm/….
The Package Standard
www.ada-auth.orgRobin Leroy
in reply to 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.
github.com/eggrobin/ada-playgr…
ada-playground/src/ada_playground.2.ada at master · eggrobin/ada-playground
GitHub🇺🇦 haxadecimal
in reply to mcc • • •Cali
in reply to mcc • • •Ludwig Vielfrass
in reply to mcc • • •I haven’t looked seriously at ADA in 30 years but it was at one time considered to be The Future™️. To many of us, it was what we considered the ultimate “bondage and discipline” language. But it did have good ideas that informed future languages.
I still don’t want to program in it now.
Daniel V.
in reply to mcc • • •Ada is the language that was used for the intro classes for the CS program I attended in Uni. I already had experience in Java at the time but someone really recommended I go through and do the Ada courses.
I dropped out and didn’t get seriously back into programming for well over a decade because of it. It set the stage for a very unappealing journey at Uni and whomever told me I should do it anyways: I hope they rot in hell.
none gender with left politics
in reply to mcc • • •Shiny Quagsire
in reply to none gender with left politics • • •mcc
in reply to Shiny Quagsire • • •Joe
in reply to mcc • • •rk: it’s hyphen-minus actually
in reply to mcc • • •A lot of the Pascal-influenced languages do that; it may go back to Algol, I don’t remember. You can do stuff like
TYPE FooA ARRAY[7..10] OF FOO;
and set the valid indexes of the array type. When ISO Pascal introduced Conformant Arrays, you could declare functions with formal parameters like
PROCEDURE MyProc(VAR x : ARRAY [low..high : INTEGER] OF INTEGER);
and low and high would be local variables set to the minimum and maximum index of the array (which may not start at 0).
Fun!
reshared this
mcc e Oblomov reshared this.
VISITE O DECORADO
in reply to mcc • • •yes, I feel seen!
Also, to add one more example, I love flexible array indexing as defined in AWK: indexes can be any number: zero, negatives, sparse series, etc. – but arrays generated by awk itself (e. g. by using 'split') are indexed starting on 1.
PsySal
in reply to mcc • • •Roger BW 😷
in reply to mcc • • •mcc
in reply to Roger BW 😷 • • •Roger BW 😷
in reply to mcc • • •mcc
in reply to Roger BW 😷 • • •cassie
in reply to mcc • • •Ruth [☕️ 👩🏻💻📚✍🏻🧵🪡🍵]
in reply to mcc • • •Riley S. Faelan
in reply to mcc • • •Oblomov
in reply to Riley S. Faelan • • •Riley S. Faelan
in reply to Oblomov • • •@oblomov MATLAB might do it because it's a mathematical convention to count matrix indices from 1.
@mcc
Uilebheist
in reply to Riley S. Faelan • • •mcc
in reply to Uilebheist • • •Oblomov
in reply to Riley S. Faelan • • •and Julia follows MATLAB quite closely (also in row vs column major, plus a lot of sub-indexing methods). Also in Julia there's a package that allows you to create arrays with arbitrary index starts, so I guess that would make it easier to port Ada or Pascal programs. It also has (recommended) array traversal iterators that work regardless of indexing choice, which is actually Very Nice™.
James Widman
in reply to Riley S. Faelan • • •Oblomov
in reply to James Widman • • •@JamesWidman @riley
true, although that's *technically* because it's lisp and the 0-th element is the head.
In[1]:= l = {1, 2, 3, 4, 5}
Out[1]= {1, 2, 3, 4, 5}
In[2]:= l[[0]]
Out[2]= List
James Widman
in reply to Oblomov • • •@oblomov @riley while we're at it, i guess nothing stops C++ users from writing:
T& operator[](size_t ix) {
assert(ix >=1);
return this->ptr[ix - 1];
}
PunnO)))
in reply to mcc • • •Early PC BASICs let you pick 0/1 indexed on a program by program basis.
Is Ada by variable, or by value held in the variable? Like if it's by value, do functions with array args have to inspect the value before accessing index 5?
mcc
in reply to PunnO))) • • •Dag Ågren ↙︎↙︎↙︎
in reply to mcc • • •Charlie
in reply to mcc • • •if I remember you can put an enum in there too!
Tbh I sorta understand why this isn't common anymore. Explosion in types for mild benefits
ask
in reply to mcc • • •Janne Moren
in reply to mcc • • •As already said, Fortran arrays start with index 1 unless you declare a different range. But also, arrays are column-major order whereas C-based languages use row-major.
Both design choices (on the part of C, to be sure) make sure you'll have extra fun if you need to port complicated numerical code from one to the other.
abadidea
in reply to mcc • • •mcc
in reply to abadidea • • •duk
in reply to mcc • • •Well, the main gimmick of ada is the typing. Types are supposed to mean much more than "a range of values" - the idea is that all of your types, even the ones that seem 'trivial' like integers, also encode intent. That includes the types you use to index into arrays.
When you do
array(1 .. 5)you're actually creating an anonymous subtype ofInteger. If you have two different types where one is not a subtype of the other, and you declare an array with those types, you have to cast between the types to switch between the two. That's Ada's way of forcing you to actually take those cases into account.mcc
in reply to duk • • •duk
in reply to mcc • • •Yep! At that point you're SOL.
There are surprisingly few guardrails in quite a few places if you don't use SPARK - especially around dynamic memory allocation.
mcc
in reply to duk • • •Marcel(le)
in reply to abadidea • • •👻 Feufochmar
in reply to Marcel(le) • • •Also, in Ada, it’s easier to load binary file as you can easily describe the memory layout of types and thus specify a binary serialisation, than to interpret text files.
mcc
in reply to 👻 Feufochmar • • •@Feufochmar @mu @0xabad1dea "in Ada, it’s easier to load binary file as you can easily describe the memory layout of types and thus specify a binary serialisation, than to interpret text files."
I will admit that the absence of a standard way to do this in C is one of my biggest pet peeves about the language.
Andrew
in reply to mcc • • •Trammell Hudson
in reply to mcc • • •Lucas Treffenstädt
in reply to mcc • • •Ratsnake Games 🔞
in reply to mcc • • •Elias Mårtenson
in reply to mcc • • •Have you tried APL? This language (thankfully not replicated in most of its successors like J or BQN) has a global variable called
⎕IO(index offset) which can be set to 0 or 1 to indicate the start index of arrays.Changing this global variable changes the language behaviour, globally.
Now, it not only changes the way you index variables, but functions that return indexes, or work with indexes also change. So a lot of basic functionality actually remains unchanged when this variable is changed. However, if you want to write a more complicated function that work independently of the value of
⎕IO, you have to be very careful.In practice, a project decides which one to use, and then you'd better never change it or you'll have a lot of problems.
It's also always fun to discuss APL in a chat, and someone shares some interesting way to solve a problem. You try it and it doesn't work, and of course it's because they used
⎕IO1.Rhialto
in reply to mcc • • •Rhialto
in reply to mcc • • •Robin Leroy
in reply to mcc • • •declare
Mem : array (Positive range 1 .. Some_Size_That_Is_Known_Here) of Integer range -1..Integer'Last;
begin
-- Do things with Mem.
end;
mcc
in reply to Robin Leroy • • •Pascal Leroy
in reply to mcc • • •There is a function form of GetLine so I would imagine that the following would work:
Line : constant String := Get_Line; -- From stdin.
or, if you have a file path:
F : File_Type;
begin
Open(F, In_File, "file/path");
declare
Line : constant String := Get_Line(F);
begin
mcc
in reply to Pascal Leroy • • •gaytabase
in reply to mcc • • •mcc
in reply to gaytabase • • •Andy Wootton
in reply to mcc • • •Daniel Correia
in reply to mcc • • •I'm very unfamilliar with Ada overall, so take this with a grain of salt; you've probably come across this context already - but I think your point about "There's really important environments [...] maybe it turns out Ada is *perfect* for this environment" is possibly spot on.
I understand that one of the main drivers of Ada's brief popularity was its adoption by the Department of Defense for safety-critical systems. Indeed, it's the main language for the Space Station's MDM processors.
In that setting, NASA's software reliability group (until recently) had a strict set of predicates called the Power of Ten[2]. Rule #3 is: *"Do not use dynamic memory allocation after initialization."* I think that meshes very well with the friction you're referring to. The same rule is laid out in MISRA standards for safe automotive software.
(in practice, I think it's highly debatable whether these prescriptions actually work - there are some very safe embedded systems that use other paradigms - but that's the working hypothesis for many of these projects)
[1] en.wikipedia.org/wiki/The_Powe…
[2] space.stackexchange.com/questi…
coding guidelines by Gerald J. Holzmann
Contributors to Wikimedia projects (Wikimedia Foundation, Inc.)mcc
in reply to Daniel Correia • • •@0xdbfb7 The fixed-memory environment is a legitimately interesting one. But it's very much not the only environment! For comparison, consider networked server software. This is an important use case which naturally needs use of dynamic memory allocation, virtual memory, and runtime file I/O, but also would benefit immensely from the safety guarantees Ada/Spark claim.
I understand some languages are narrow-application, but Ada is sold as, and feels designed as, a general purpose language…
Andy Wootton
in reply to mcc • • •✧✦Catherine✦✧
in reply to mcc • • •this is why i don't use VHDL 😁
"it seems good but is a pain in the ass to actually use" is like, The ADA/VHDL experience
Joe
in reply to mcc • • •Knut Branson
in reply to mcc • • •Alyssa Coghlan
in reply to mcc • • •Checking your list of candidate languages, one that's not currently listed but seems likely to inspire a similar sense of "interesting in theory, annoying in practice" is Eiffel: en.m.wikipedia.org/wiki/Eiffel…
I learned a lot about OOP in general by learning Eiffel in particular, but I never used it for any actual practical purpose.
programming language
Contributors to Wikimedia projects (Wikimedia Foundation, Inc.)mcc
in reply to Alyssa Coghlan • • •Euclidian Ace
in reply to mcc • • •hopefully this comes off as helpful and not an "um actually ada's great" cause ergonomics and learning materials are almost non-existent, it makes up a lot of its own jargon, and as you said, gnat's errors are dogshit.
`Text_IO.Get_Line` has overloads that take a file handle (or `File_Type`) and return a `String`
Also `Option` kind of exists with the catchy name `Ada.Containers.Indefinite_Holder`
godbolt.org/z/KKoGK97M4
Compiler Explorer - Ada
godbolt.orgmcc
in reply to Euclidian Ace • • •mcc reshared this.
Chris [list of emoji]
in reply to mcc • • •