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

@dibblego @psnively in other words, just because you're writing an expression that represents a proof, doesn't mean it's the same technique.