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
I'm very interested in knowing what array languages they were researching. The only thing I can find is Nile[1] but from the examples it doesn't look like an array language to me.
> Dynamicland's new research website will be up in the spring.
> current status:
> 1156 pages
> 11,120 images
> 693 videos
> 56 pdfs
(https://nitter.privacydev.net/worrydream/status/175311604225...)
noticeably missing from this list is source code, unless that's on the 1156 pages
i'm sure i'll devour them eagerly, though
however, i do agree that there are some advances made since then that he doesn't fully appreciate, things like the importance of free-software licensing, roy fielding's work on architectural styles, recent advances in formal methods and functional programming, and the web's principle of least power