1. 6



  2. 7

    I’ve been doing a fair amount of AVR work in Ada lately, as well; at some point, I’ll probably switch to using Spark. It’s nice to have strict typing and formal semantics on even these devices.

    1. 2

      One of the (many) items on my (ever growing) todo list is to experiment with Ada, SPIN and model-checking embedded-systems software.

      1. 1

        What’s SPIN?

        That’s a new one to me.

        1. 2

          @angersock Spin is a model-checker i.e. you provide a formal specification of a program (usually a concurrent one) and it is able to prove some properties (i.e. absence of deadlocks), it also features tools to aid you in extracting [formal] models from C programs. I was speculating that Ada should be more friendly with respect to formal model extraction and hence use with Spin.

      2. 2

        Thanks, I’d never heard of Spark. Do you have much experience with it?

        1. 1

          I’ve only just started using it, actually.