Ah ha! I knew _SOMEBODY_ had to do it. [imperative programming meets logic meets proofs meets axioms meets formal meets DRILL SARGENT ITS TRUE ‘CAUSE I SAID IT IS] I’ve been looking for a Calculus for Imperative Programming, something that uses the style of reasoning used in imperative languages, whether BASIC or C or any number of “Do this! Now do that! “This” is True! But Now “This” is False!” Do That 27 times, doing That to This, until This is now the same as Some Other Thing” “Do it Again!” “Do This when Apples are Pears, That when Oranges Eat Floorboards, and the Other Thing when 7 Apples are 8 Pears but Floorboards No longer exist” So I think I found it. It _should_ tie together a formal calculus, and might be a proof system I can actually *read* because I understand Turing’s / Church’s ways. Church’s Lambda is fantastic but it’s a little *too* open. Our computers were built on Turing’s ideas but Turing’s a “get er done” process but there’s hardly anything formal about it except, “Hey guys, this works. Shut up and GOTO MEMORY LOCATION AH7 for the next counter in the stack pop” Anyway, Assignment Calculus: A Pure Imperative Reasoning Language by M Bender (2010)

Ah ha! I knew _SOMEBODY_ had to do it.
[imperative programming meets logic meets proofs meets axioms meets formal meets DRILL SARGENT ITS TRUE ‘CAUSE I SAID IT IS]

I’ve been looking for a Calculus for Imperative Programming, something that uses the style of reasoning used in imperative languages, whether BASIC or C or any number of “Do this! Now do that! “This” is True! But Now “This” is False!” Do That 27 times, doing That to This, until This is now the same as Some Other Thing” “Do it Again!” “Do This when Apples are Pears, That when Oranges Eat Floorboards, and the Other Thing when 7 Apples are 8 Pears but Floorboards No longer exist”

So I think I found it. It _should_ tie together a formal calculus, and might be a proof system I can actually *read* because I understand Turing’s / Church’s ways.

Church’s Lambda is fantastic but it’s a little *too* open. Our computers were built on Turing’s ideas but Turing’s a “get er done” process but there’s hardly anything formal about it except, “Hey guys, this works. Shut up and GOTO MEMORY LOCATION AH7 for the next counter in the stack pop”

Anyway,

Assignment Calculus: A Pure Imperative Reasoning Language
by M Bender (2010)

[responsivevoice_button voice="US English Male"]