ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Dependent Types: Runtime assertions at compile time...whaaa? (S04E08)"
Episode Synopsis
Dependent types are a more expressive type system in programming languages used to catch a larger class of errors at compile time. What are would be typically assertions at runtime can now be caught at compile time.Show notes:Proposition as TypesParse, Don’t Validation“Scala vs Idris: Dependent types, now and in the future”Resources:http://www.e-pig.org/downloads/ydtm.pdfhttps://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196Proof Theory Impressionism: Blurring the Curry-Howard LineType Systems - The Good, Bad and UglyDependent types for practical useIdris: Practical Dependent Types with Practical ExamplesMaking Illegal States unrepresentableCan types replace validationhttps://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf
More episodes of the podcast The Technium
LLMs eat software development
13/04/2023
ChatGPT Part 2 (S04E03)
12/01/2023
ChatGPT Part 1 (S04E03)
05/01/2023
Nix Package Management (S04E02)
21/12/2022
Visual Programming (S04 E01)
07/12/2022
In God we trust