2021-07-15 02:39:36 remexre, tangentstorm: I formally verified XOR swap in C, see https://gist.github.com/siraben/d2ad58914166d5f6139b03b1b503ed6c
2021-07-15 02:40:36 the spec I wrote was (in words)
2021-07-15 02:40:36 Let a and b be unsigned int pointers to values n and m respectively, with respective writable shares sh1 and sh2, and a ≠ b. Then the postcondition of XorSwap states that a and b will point to m and n respectively.
2021-07-15 05:07:24 what's the .v language, siraben ?
2021-07-15 05:07:33 tangentstorm: Coq
2021-07-15 05:09:25 https://softwarefoundations.cis.upenn.edu/vc-current/Verif_sumarray.html ?
2021-07-15 05:17:31 proof assistants are really cool.. i wish coq in particular had a mode where you could record the actual proof it constructs instead of just the instructions for how to construct the proof.
2021-07-15 05:20:43 isabelle and lean let you write 'calculation-style' proofs where you show the expression you believe to be true (or equivalent to the expression on the previous line) at each step.
2021-07-15 05:20:46 ex: https://github.com/tangentstorm/tangentlabs/blob/master/isar/SumOfRange.thy
2021-07-15 05:22:03 isabelle also lets you replace the syntax for the object language (the part in double quotes) with whatever you want, but I've never figured out how to do it.
2021-07-15 05:24:43 i'm very slowly working up to building a proof assistant in a forth-like vm... i'd really like to see these tools be more accessible and programmer-oriented someday.
2021-07-15 06:08:58 tangentstorm: yeah using verifiable C
2021-07-15 06:09:02 I'm going through that book
2021-07-15 06:09:58 tangentstorm: calculation style is nice to read but can slow down writing the proof
2021-07-15 06:10:06 e.g. agda has a calculation style as well
2021-07-15 06:10:31 tangentstorm: nice, that isabelle proof is readable
2021-07-15 17:47:10 maw
2021-07-15 17:51:52 wam