3 ms·
A number of modern languages (F-star, LEAN, Coq, Agda, Idris, …) use Dependent Types. It enables you to prove code correct using just the type system. Very cool
by mbrodersen 4y ago
A number of modern languages (F-star, LEAN, Coq, Agda, Idris, …) use Dependent Types. It enables you to prove code correct using just the type system. Very cool.
I highly recommend the book “Type Driven Development”. I prefer that to “The Little Typer”.