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

• libaco

  3 3,437 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.

• hylo

  54 1,104 9.9 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.

• InfluxDB

  www.influxdata.com sponsored

  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.

  

• eff

  18 546 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.

• typedlua

  3 552 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.

• FStar

  42 2,562 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.

• Idris2

  39 2,395 9.6 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.

• seL4

  60 4,530 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.

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

• Agda

  27 2,368 9.8 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.

• lean4

  53 3,714 9.9 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.

• dafny

  31 2,665 9.7 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.

• fully-homomorphic-encryption

  19 3,453 7.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.

• coq

  87 4,602 10.0 OCaml

  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

  33 12,921 9.4 Scala

  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

  8 57 5.2

  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

  25 1,224 6.4 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.

• SaaSHub

  www.saashub.com sponsored

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

  

Suggest a related project