What are the current hot topics in type theory and static analysis?

This page summarizes the projects mentioned and recommended in the original post on /r/ProgrammingLanguages
#Dependent Types #proof-assistant #programming-language #Verification #theorem-proving

Our great sponsors
  • InfluxDB - Collect and Analyze Billions of Data Points in Real Time
  • Onboard AI - Learn any GitHub repo in 59 seconds
  • SonarLint - Clean code begins in your IDE with SonarLint
  • Revelo Payroll - Free Global Payroll designed for tech teams
Our great sponsors

  • libaco

    A blazing fast and lightweight C asymmetric coroutine library 💎 ⛅🚀⛅🌞

    Coroutines, async/await and general multicore support in the type system. Most languages by now either have some variant of async / await (JavaScript, Kotlin, Swift, Rust) or super-lightweight threads (Go, Elixir, Java via Project Loom), or they just have Monads which supersede coroutines entirely (Haskell, Scala). It's at the point where some say a language isn't suitable for production if it doesn't have good multicore support (also see Rust speeding through getting async/await even though they already have Send + Sync). Even Python and C++ have coroutines now, and of course there is a coroutine library for C which uses macros and low-level magic.

  • hylo

    The Hylo programming language

    Linear/affine (substructural) types. Rust has them and is doing great, Haskell has implemented them as a “new experimental”-kind of thing. Other languages are looking to incorporate some variant or alternative to Rust’s borrowing rules: Mojo (the hyped-up “AI” language) includes them, and Val-lang has mutable value semantics which are similar.

  • InfluxDB

    Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.

  • eff

    🚧 a work in progress effect system for Haskell 🚧 (by hasura)

    Effect systems and Algebraic effects. ocaml has just released a stripped-down effect system. People are also working on Effect systems for Haskell (eff, fused-effects, effet). Koka is a language built with effects first and foremost and it’s rapidly gaining popularity. Unison also has effects.

  • typedlua

    An Optional Type System for Lua

    Gradual typing. This is what TypeScript is: you have some typed values and untyped values, and want to verify and possibly optimize the typed code while permitting the untyped code to compile. Besides JavaScript/TypeScript, you'll find gradual typing on pretty much any other popular untyped language including Python, Lua, and Racket. Mojo is also going to have gradual typing.

  • FStar

    A Proof-oriented Programming Language

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • Idris2

    A purely functional programming language with first class types

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • seL4

    The seL4 microkernel

    Formal methods. This is not in most general-purpose programming languages and probably never will be (maybe we'll see formal methods to verify unsafe code in Rust...) because it's a ton of boilerplate (you have to help the compiler type-check your code) and also extremely complicated. However, formal methods is very important for proving code secure, such as sel4 (microkernel formally verified to not have bugs or be exploitable) which has just received the ACM Software Systems Award 3 days ago.

  • Onboard AI

    Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.

  • Agda

    Agda is a dependently typed programming language / interactive theorem prover.

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • lean4

    Lean 4 programming language and theorem prover

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • dafny

    Dafny is a verification-aware programming language

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • fully-homomorphic-encryption

    An FHE compiler for C++

    Secure computing. This includes Fully Homomorphic Encryption AKA FHE, of which there is a language/compiler which just got released and Google's older FHE compiler. FHE is probably more "compiler" than "type system", e.g. Google's compiler works on C++. Also Security Type Systems which include Oblivious data structures and Oblivious ADTs.

  • coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

    Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

  • Akka

    Build highly concurrent, distributed, and resilient message-driven applications on the JVM

    First-class distributed and multicore computing. Swift has first-class “actors” and “distributed” methods. Unison, Erlang, and Elixir are built with distributed being one of the #1 concerns. Though first-class is not super common and I don't really expect it to be because usually libraries are enough (e.g. Scala has Akka and is used WIDELY for distributed); whereas something like linear types and typed effects, you can't emulate in a library.

  • rfcs

    RFC process for Bytecode Alliance projects (by bytecodealliance)

    I would add that Equality saturation/E-graphs has become quite a hot topic recently, since their POPL21 paper, with workshops dedicated to applications of e-graphs. They have even recently been added to Cranelift as an IR for optimizations.

  • egg

    egg is a flexible, high-performance e-graph library (by egraphs-good)

    I would add that Equality saturation/E-graphs has become quite a hot topic recently, since their POPL21 paper, with workshops dedicated to applications of e-graphs. They have even recently been added to Cranelift as an IR for optimizations.

  • SonarLint

    Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts