Tony Morris

@psnively perhaps likely, but all of these high level phrases are sort of puzzling because their semantic content doesn't tell you much

@psnively e.g., if you say "programs are proofs" what does that mean? Does it mean that if you can write rails apps then you can do proofs?

@krismicinski @psnively See Curry-Howard Isomorphism.

@dibblego @psnively sure, I've done a lot of work "programming" in Coq. But the mechanics of proof development don't "feel like" programming

@krismicinski @dibblego @psnively then use Agda instead :)

@copumpkin @krismicinski @psnively Haha best response. Seriously what does what it "feels like" become relevant? I ain't no homeopath.

@dibblego @krismicinski @psnively writing proofs (even in Agda) definitely involves different "muscles" than those used in e.g., Haskell