[elcritch]

Interesting write-up! I've barely used Rust but had/have a similar feeling. It's really more akin to C++ and really powerful but also pretty complex. For smaller MCU projects it just feels like overkill.

> Microcontrollers have a lot of functionality packed into the pins (see the STM32 "Alternate Function" datasheet tables). Trying to model all of that using ownership of zero-sized generic types would strike me as a "when all you have is a hammer"-type situation.

The whole idea of utilizing TLA+ for a system level check really does seem like something that would be awesome, even if it's unclear how much effort it'd require to instrument an entire project with TLA+.

> the problem is simply that Rust makes it difficult to conceptually iterate over distinct types (regardless if such iteration occurs at runtime via a loop or at compile-time via an unrolled loop, as per Zig's `inline for`).

Rust just brings a lot of incidental complexity along and still makes some things really difficult. Perhaps it's better in the long run but it's just harder to work with.

Similarly, I wanted a simpler language than Rust and started using Nim last summer for embedded projects. Primarily since it compiles to C which let's me target ESP32's and existing RTOS'es without rewriting everything or trying to get LLVM based tools to work with GCC ones. However, it also embraces `lazy` compilation approach to code and it's standard library.

I wanted to try your example in Nim. Here's roughly how your example would look in Nim (it appears to duck type fine as well):

    var
      # normally just import these from the C headers as-is
      # but this lets us run it
      p0* : RefPort0 = addr port0
      p1* : RefPort1 = addr port1

    var rows = (
         ( port: p1, pin: 0 ),
         ( port: p1, pin: 1 ),
         ( port: p1, pin: 2 ),
         ( port: p1, pin: 4 ),
      )

    var cols = (
        (port: p0, pin: 13 ),
        (port: p1, pin: 15 ),
        ...
        (port: p0, pin: 2 )
      )

    proc initKeyboardGPIO() =
      rows[0].port.pin[rows[0].pin].dir = output

      for item in rows.fields: 
        item.port.pin[item.pin].dir = output

Full example: https://gist.github.com/elcritch/1c8279418fc62f5e941b41a5df4...

I've toyed with the thought of adding TLA+ hooks into Nim similar to Dr Nim (https://nim-lang.github.io/Nim/drnim.html) using the effect system. Not sure if Zig has an effect system for a similar setup.