The Case for Formal Verification (2013)

Post by dllthomas » Mon, Apr 21, 2014, 7:44 PM UTC

tluyben2 wrote: post #78

jnbiche wrote: post #36

Earlier quoted context omitted.

I've also been playing around with these two. I have a little Haskell and some OCaml, but very little understanding of the mathmatics involved in dependent typing, so I'm struggling but still very interested. Wish there were an accessible guide like "Learn you a Haskell" for Idris. By the way, for anyone interested in these two languages with dependent typing, you can try out both Idris and F* online, without install…

Cannot edit for reason, but I thought I would mention, as this is of vital importance to me when i'm learning something new, that both Idris and F* are open source; https://github.com/nikswamy/FStar (Apache) https://github.com/idris-lang/Idris-dev (do whatever, just retain copyright)

Post by eli_gottlieb » Tue, Apr 22, 2014, 1:47 PM UTC

lmm wrote: post #69

dkarapetyan wrote: post #43

Earlier quoted context omitted.

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

> Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? I gained some evidence. Do you refuse to accept the theory of gravity because we've only measured some examples where F Gm_1m_2 / r^2, not proven it from first principles?