00:00:00 --- log: started forth/21.07.15
01:05:59 --- join: Glider_IRC_ joined #forth
01:08:50 --- quit: Glider_IRC (Ping timeout: 120 seconds)
02:07:48 <cbridge_> <tangentstorm> what's the .v language, siraben ?
02:07:56 <cbridge_> <siraben> tangentstorm: Coq
02:09:49 <cbridge_> <tangentstorm> https://softwarefoundations.cis.upenn.edu/vc-current/Verif_sumarray.html ?
02:17:55 <cbridge_> <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.
02:21:06 <cbridge_> <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.    
02:21:09 <cbridge_> <tangentstorm> ex: https://github.com/tangentstorm/tangentlabs/blob/master/isar/SumOfRange.thy
02:22:28 <cbridge_> <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.
02:25:06 <cbridge_> <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.
02:49:24 --- quit: lonjil (Ping timeout: 120 seconds)
02:51:42 --- join: lonjil joined #forth
03:09:21 <cbridge_> <siraben> tangentstorm: yeah using verifiable C
03:09:26 <cbridge_> <siraben> I'm going through that book
03:10:23 <cbridge_> <siraben> tangentstorm: calculation style is nice to read but can slow down writing the proof
03:10:31 <cbridge_> <siraben> e.g. agda has a calculation style as well
03:10:56 <cbridge_> <siraben> tangentstorm: nice, that isabelle proof is readable
05:27:47 --- quit: Glider_IRC_ (Connection closed)
05:28:35 --- join: Glider_IRC_ joined #forth
12:31:20 --- join: mark4 joined #forth
13:06:19 --- join: Glider_IRC__ joined #forth
13:09:12 --- quit: Glider_IRC_ (Ping timeout: 120 seconds)
14:47:34 <cbridge_> <dave0> maw
14:52:16 <cbridge_> <lispmacs[work]> wam
16:44:29 --- quit: proteusguy (Ping timeout: 120 seconds)
16:55:35 --- join: X-Scale` joined #forth
16:55:40 --- quit: X-Scale (Ping timeout: 120 seconds)
16:56:39 --- nick: X-Scale` -> X-Scale
16:58:34 --- join: proteusguy joined #forth
17:26:49 --- join: Glider_IRC_ joined #forth
17:28:42 --- quit: Glider_IRC__ (Ping timeout: 120 seconds)
23:59:59 --- log: ended forth/21.07.15