This page includes the programming languages I like and use.
These are the languages that I love and and use constantly.
| Language | Role | Core idea |
|---|---|---|
| Rust | Systems programming | Ownership + zero-cost abstraction |
| OCaml | Compilers & symbolic systems | Algebraic data types + modules + inference |
| Lean | Formal verification | Dependent types + theorem proving |
| Kotlin | Application development | Pragmatic static typing + JVM ecosystem |
| Julia | Scientific computing | Multiple dispatch + runtime specialization |
| PostgreSQL | Relational data systems | Declarative querying + transactional consistency |
| Typst | Technical typesetting | Programmable document composition with modern syntax |
These are the languages I found interesting.
| Language | Role | Core idea |
|---|---|---|
| Haskell | Pure functional programming | Laziness, typeclasses, higher-kinded abstractions, typed effects |
| Racket | Language-oriented programming | Macros, DSLs, extensible languages |
| Pharo | Live object systems | Message passing, reflection, image-based development |
| Prolog | Logic programming | Unification, relations, backtracking |
| Elixir / Gleam | Concurrent distributed systems | Actors, supervision, BEAM fault tolerance |
| Zig | Modern systems design | Explicit control, comptime, minimal abstraction machinery |
| C# | Evolving industrial language | LINQ, async/await, generics, gradual modernization |
| F# | Industrial functional programming | ML-style FP inside the .NET ecosystem |
| Swift | Value-oriented systems/application design | Protocols, value semantics, ownership, structured concurrency |
| Scala 3 | Advanced industrial type systems | Contextual abstractions, unions/intersections, match types |
| Go | Minimalist language design | Structural interfaces, simple concurrency, deliberate restraint |
| PureScript | Typed functional web programming | Haskell-style FP, row polymorphism, JavaScript interop |
| Elm | Functional UI design | TEA architecture, pure state transitions, friendly static types |
| MoonBit | Wasm-first language design | Integrated toolchain, Wasm, modern compiler engineering |
| Agda | Dependently typed programming | Proofs as programs, dependent pattern matching |
| Idris 2 | Resource-aware dependent programming | Quantitative type theory + dependent types |
| F* | Program verification | Refinements, dependent types, effects, SMT automation |
| Koka | Effect-system research | Algebraic effects, handlers, effect polymorphism |
| Flix | Effect-oriented functional/logic programming | Inferred effects + regions + handlers + embedded Datalog |
| Granule | Quantitative type-system research | Graded modal and linear types |
| Arend | HoTT-oriented theorem proving | Univalence, paths, higher-dimensional equality |
| Unison | Alternative code architecture | Content-addressed code + algebraic effects |
| Futhark | Parallel functional computing | Data-parallel arrays and optimizing compilation |
| Roc | Experimental functional design | Structural typing, platform/application separation |
| Mojo | Experimental high-performance design | Ownership, specialization, numerical/systems programming |
These are the languages that are impossible to avoid.
| Language / Tool | Role | Core idea |
|---|---|---|
| C / C++ | Native systems & interoperability | Manual control, performance, ABI-level integration |
| Python | Scripting & ecosystem glue | Dynamic programming, rapid iteration, huge ecosystem |
| JavaScript / TypeScript | Web platform | Browser ubiquity + dynamic/gradual structural typing |
| Java | JVM ecosystem | Managed OO, portability, enterprise libraries |
| Shell | System automation | Processes, pipelines, command composition |
| LaTeX | Academic typesetting | Macro-based document preparation + mathematical notation |
| HTML / CSS | Web documents & presentation | Declarative structure + styling |
| Assembly | Machine-level programming | Registers, instructions, calling conventions, memory layout |