There's the so-called 'B Method', which seems very similar to this on the programming language side. I haven't checked the proof language so that may be very di

There's the so-called 'B Method', which seems very similar to this on the programming language side. I haven't checked the proof language so that may be very different. I've got a two-parter on my blog giving a glimpse of B's programming language[1] and proof language[2]. [1] https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_programmers_(part_1)/ https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_progr... [2] https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_programmers_(part_2)/ https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_progr...