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

1. libaco

   1 3 3,568 10.0 C

   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.

2. InfluxDB

   www.influxdata.com featured

   InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

   

3. hylo

   2 60 1,342 9.2 Swift

   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.

4. eff

   3 18 557 0.0 Haskell

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

5. typedlua

   4 4 577 10.0 Lua

   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.

6. FStar

   5 48 2,835 9.9 F*

   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.

7. Idris2

   6 39 2,656 9.0 Idris

   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.

8. seL4

   7 67 4,922 9.0 C

   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.

9. SaaSHub

   www.saashub.com featured

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

   

10. Agda

    8 27 2,627 9.9 Haskell

    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.

11. lean4

    9 62 5,460 10.0 Lean

    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.

12. dafny

    10 38 3,064 9.5 C#

    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.

13. fully-homomorphic-encryption

    11 19 3,568 0.0 C++

    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.

14. rocq

    12 88 5,097 10.0 OCaml

    The Rocq Prover is an interactive theorem prover, or proof assistant. 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.

15. Akka

    13 33 13,155 9.3 Scala

    A platform to build and run apps that are elastic, agile, and resilient. SDK, libraries, and hosted environments.

    

    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.

16. rfcs

    14 9 65 6.5

    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.

17. egg

    15 25 1,486 7.1 Rust

    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.

18. SaaSHub

    www.saashub.com featured

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

    

Suggest a related project