4 ms·

And static type calculus as seen in the MLs, Haskell, and lately C++.

by angiosperm 3y ago

kragen 3y ago
yes, although recent advances in functional programming and formal methods go a lot further than that
- linguae 3y ago
  This is really interesting; it’s really cool to think about the “statics” and “dynamics” of programming, and I while I have a basic understanding of functional programming (both the dynamic world of Scheme and the static world of languages like Standard ML and Haskell), I’m unfamiliar with these recent advances in functional programming and formal analysis. I’m wondering if you could share some links or references to some of this material?
  - kragen 3y ago
    i'm not the best person to ask, and i don't really know where to start tla+ is getting uptake in industry, idris is sort of making dependent types practical, acl2 has more and more stuff in it, pvs is still around and still improving, adam chlipala keeps blogging cool stuff, so does hillel wayne, sel4 is an entire formally-proven-secure microkernel, you can try compcert on godbolt's compiler explorer, ləɐn has formalized significant mathematical definitions that working mathematicians use actively while metamath has an extremely convincing approach to proof and an ever-growing body of proofs of basic math, smt solvers like z3 are able to solve bigger and bigger problems and therefore able to tackle bigger subproblems of verifying software (and are easily apt installable and callable from python or from cprover's cbmc), cryptocurrency smart contracts have an incentive to be correct in a way that no previous software did (and people are applying at least idris to at least ethereum), ... a thing i saw recently that was really impressive to me was parsley, by the main author of pvs as well as some other people: http://spw20.langsec.org/papers/parsley-langsec2020.pdf http://spw20.langsec.org/papers/parsley-langsec2020.pdf
zelphirkalt 3y ago
Pretty sure he would appreciate it for the guarantees those come with, but criticize them for being dead programs, that are not alive like for example the internet, one of his examples for systems, that started and from that moment on have not been taken offline to be changed.
- kragen 3y ago
  he might not appreciate us pretending we know what he thinks ;)

And static type calculus as seen in the MLs, Haskell, and lately C++.

kragen 3y ago

yes, although recent advances in functional programming and formal methods go a lot further than that

linguae 3y ago
This is really interesting; it’s really cool to think about the “statics” and “dynamics” of programming, and I while I have a basic understanding of functional programming (both the dynamic world of Scheme and the static world of languages like Standard ML and Haskell), I’m unfamiliar with these recent advances in functional programming and formal analysis. I’m wondering if you could share some links or references to some of this material?
- kragen 3y ago
  i'm not the best person to ask, and i don't really know where to start tla+ is getting uptake in industry, idris is sort of making dependent types practical, acl2 has more and more stuff in it, pvs is still around and still improving, adam chlipala keeps blogging cool stuff, so does hillel wayne, sel4 is an entire formally-proven-secure microkernel, you can try compcert on godbolt's compiler explorer, ləɐn has formalized significant mathematical definitions that working mathematicians use actively while metamath has an extremely convincing approach to proof and an ever-growing body of proofs of basic math, smt solvers like z3 are able to solve bigger and bigger problems and therefore able to tackle bigger subproblems of verifying software (and are easily apt installable and callable from python or from cprover's cbmc), cryptocurrency smart contracts have an incentive to be correct in a way that no previous software did (and people are applying at least idris to at least ethereum), ... a thing i saw recently that was really impressive to me was parsley, by the main author of pvs as well as some other people: http://spw20.langsec.org/papers/parsley-langsec2020.pdf http://spw20.langsec.org/papers/parsley-langsec2020.pdf

zelphirkalt 3y ago

Pretty sure he would appreciate it for the guarantees those come with, but criticize them for being dead programs, that are not alive like for example the internet, one of his examples for systems, that started and from that moment on have not been taken offline to be changed.

kragen 3y ago
he might not appreciate us pretending we know what he thinks ;)