Our great sponsors
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
Unison is definitely very cool. I used it myself for a work thing and it was quite useful. I'm just surprised every time I go back to https://github.com/bcpierce00/unison/issues/375 and see the wire protocol still doesn't has been fixed to work across different versions.
A recent book in the same vein: The Hitchhiker's Guide to Logical Verification
https://github.com/blanchette/logical_verification_2020
This is a tipping point work making the case that type theory is like a musician reading sheet music. Sure, the Beatles couldn't, but... Anyone developing a new programming language should understand languages at the level of Lean, even if the common uses of their constructs aren't theorem proving. The analogies are mind-blowing. Monadic parsing is the same thing as meta-programming tactics? I'm still wrapping my head arond that one.
Related posts
- Austral: A systems language with linear types. (2021)
- Lolita: A tagless, dependently typed, self-aware programming language
- Semgrep – Find bugs and enforce code standards
- Toy autograd engine in OCaml with Apple Accelerate back end
- Application Security - Bridging Frontend and Cybersecurity: What is Application Security?