My personal views on languages I've used (or not).
OCaml - An impressive higher-order imperative language that's at a sweet spot between expressiveness and practicality. I'm still not used to its module system and untyped effects, but I do enjoy the experience of writing OCaml code.
Coq - The go-to proof assistant for me. Good ecosystem and community, and I'm also a fan of tactics. But things can get really messy when it comes to Ltac and dependent types. One day I might try out Lean. Sorry, Coq xD
Rust - Finally, an industrial language with ADT, typeclass(-like stuff), affine types, and a core team that REALLY cares about soundness! Was my first choice for hobby projects before I met OCaml.
Python - I still use it for quick prototyping and data analysis. Be hold the evil power of monkey and duck stuff!
Haskell - It traumatized my friend with endless monad transformers and chrome-like HLS (in terms of memory usage), so I haven't tried it yet. But hey, who can resist the temptation of purity and laziness? Going to try it out. Please pray for my mental health.
C++ - Meh. Hard to learn, hard to use, hard to debug. Not my cup of tea.
Go - It has a good runtime and really impressive compilation speed. That's all the good things I can say about it.
HTML/CSS/JS - I use them each time I need to update my website or write a GUI.
Visual Basic - My first programming language. Look! It has effect handlers! (Just kidding. I'm not sure whether "err: Resume Next"s are true effect handlers.)
Random side project idea: coq verified staging (or partial evaluation) on lambda calculus with nat (let + sharing) using interaction tree
It’s not that semantics is the syntax. It’s just that semantics has its own syntax. Human needs syntax to express abstract things.
lambda term is to SSOS
as SSOS is to a state transition system
as language is to its denotational semantics
as metalanguage is to the math object
“PL is a lot like quantum field theory in that everything is described in terms of creation and annihilation operators, or introduction and elimination forms”
So true 😂
Can we do it someday?
I’m so confused about Mathematics.
algebra: (carrier: Set) * (ops: Ops(s)) * (a: Axioms(s, o))
initial algebra: ops -> a -> a certain (carrier * ops * a)
free algebra: ops -> a -> a set of (carrier * ops * a)
So, what exactly is algebra??
Are operational semantics kinds of denotational semantics? They denote a language to a TRS.
It’s probably meaningless to play with terms anyway. Just joking ;)