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.)
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??
“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 😂
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
Can we do it someday?
Random side project idea: coq verified staging (or partial evaluation) on lambda calculus with nat (let + sharing) using interaction tree
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 ;)