Correct by Construction

Hosted by Coding Dojos Eindhoven

Tweet Share Share

Happy new year, happy new coding dojo!! On January 23 from 17:00 – 21.00, we invite you to join us at the High Tech Campus in HTC33 for a very special one, which will be given by guest host Rodolfo Hansen. Rodolfo is a constructive programming advocate and competency lead for the Software Center of Excellence at Philips. He is currently training software development teams in writing code that is correct by construction and has contributed to multiple open source projects most recently in the typelevel Scala community as well as the Spacemacs editor distribution.

This coding dojo is about using a few simple guiding principles when developing your software, so that you gain the ability to (formally) prove the correctness or the code. This is of course very nice because now you can say to your product owner: “hey, I can prove this works correctly, no bugs; if it’s not what you wanted, you didn’t explain well enough!” Well, that’s my understanding of it, maybe I’d better let Rodolfo introduce it:

The workshop introduces the three restrictions of Constructive Programming:

  • Totality
  • Referential Transparency
  • Termination

Including hands-on exercises on how these restrictions grant you the ability to build actual proofs of correctness and leverage what mathematics has discovered about composition in the code you write.

We will re-discover logic, from the perspective of types, do some exercises around 'fixing' code to comply with these restrictions and take a peek into the higher order compositions that arise from a "Constructive" approach to software engineering. After this workshop you should be able to connect many ideas to each other, in ways you might have not considered before; like: the halting problem, minimal logic, category theory, formal verification of software systems, composition, the expression problem, higher order logic and bi-directional transformations.

The exercises will be in Scala. You don’t need to know or learn Scala, that’s fine, but please prepare by installing Scala support in your favourite IDE, or install the Ammonite-REPL on your machine by following these instructions. For this coding dojo it is probably a good idea if your role is developing software; other related disciplines may find this a bit hard to grasp. But if that’s you and you're up for a challenge, you're most welcome :)

So, like usually:

  • Please indicate if you’re joining by signing up on GetTogether or by accepting this calendar invitation if that’s how you’re receiving it.
  • Free dinner donated by our generous boss Ralph Holdorp!
  • Let us know if (a) you have special dietary wishes, and/or (b) you need us to arrange access to the building for you.
  • Please forward this to anyone who may be interested!

Best regards,

Stefan & Mark

P.S. If you enjoyed our coding dojos about Clojure last year: on Wednesday January 15 there is a meetup about Clojure here in Eindhoven. See the meetup page for more information.

Jan. 23, 2020, 5 p.m. - Jan. 23, 2020, 9 p.m.


    Jan. 10, 2020, 1:17 p.m.

    This timeslot is overlapping with a 040coders event. ( Would it be possible for you to check eachothers calendar in the future? I really would have liked joining both events.

    Jan. 10, 2020, 1:26 p.m.

    Ah that's unfortunate, thanks for pointing that out Kees-Jan. We will pay more attention to that next time!

    Jan. 12, 2020, 8:19 p.m.


Attendees (3)

Rob Yes