2021-07-15 02:39:36 <siraben     > remexre, tangentstorm: I formally verified XOR swap in C, see https://gist.github.com/siraben/d2ad58914166d5f6139b03b1b503ed6c
2021-07-15 02:40:36 <siraben     > the spec I wrote was (in words)
2021-07-15 02:40:36 <siraben     > 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 <tangentstorm> what's the .v language, siraben ?
2021-07-15 05:07:33 <siraben     > tangentstorm: Coq
2021-07-15 05:09:25 <tangentstorm> https://softwarefoundations.cis.upenn.edu/vc-current/Verif_sumarray.html ?
2021-07-15 05:17:31 <tangentstorm> 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 <tangentstorm> 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 <tangentstorm> ex: https://github.com/tangentstorm/tangentlabs/blob/master/isar/SumOfRange.thy
2021-07-15 05:22:03 <tangentstorm> 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 <tangentstorm> 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 <siraben     > tangentstorm: yeah using verifiable C
2021-07-15 06:09:02 <siraben     > I'm going through that book
2021-07-15 06:09:58 <siraben     > tangentstorm: calculation style is nice to read but can slow down writing the proof
2021-07-15 06:10:06 <siraben     > e.g. agda has a calculation style as well
2021-07-15 06:10:31 <siraben     > tangentstorm: nice, that isabelle proof is readable
2021-07-15 17:47:10 <dave0       > maw
2021-07-15 17:51:52 <lispmacs[work]> wam