I'm working on modernizing Rosetta Code's infrastructure. Starting with communications. Please accept this time-limited open invite to RC's Slack.. --Michael Mol (talk) 20:59, 30 May 2020 (UTC)


From Rosetta Code
My Favorite Languages
Language Proficiency
Ada Competent
SPARK Expert

My Experience[edit]

Almost all my experience is in the field of embedded systems.

Since 1992 I have worked on high-integrity applications, with most of that work using SPARK. Further information can be found at my SparkSure home page.

SPARK Proof[edit]

I have a particular interest in the use of SPARK for the formal proof of program properties and I have written some tutorials on this.

SPARK is a uniquely capable language for proof as it can be used for industrial scale applications but is also a completely unambiguous language - so formal proofs become meaningful.