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

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.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • 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.

  • 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.

    InfluxDB logo
  • 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.

  • 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.

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
  • 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.

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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

  • Lean4 helped Terence Tao discover a small bug in his recent paper

    10 projects | news.ycombinator.com | 27 Oct 2023
  • If You've Got Enough Money, It's All 'Lawful'

    2 projects | /r/WorkReform | 13 May 2023
  • Paper from 2021 claims P=NP with poorly specified algorithm for maximum clique using dynamical systems theory

    1 project | /r/computerscience | 12 Jan 2023
  • Low-level format file of mathlib

    1 project | /r/leanprover | 21 Dec 2022
  • [Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use

    2 projects | /r/INAT | 9 Nov 2022