The Firehose

André Muricy presents Agda, a dependently typed programming language, and its philosophy, motivation, and underlying theory. Agda aims to increase confidence in the correctness of code by allowing the expression of specific shapes or types for functions, reducing cognitive workload.

André introduces the concept of dependent types, which bridge the gap between human intention and machine code. He also discusses the importance of striking a balance between convenience and correctness in programming and the use of Agda mode for facilitating Agda programming in Integrated Development Environments (IDEs).

The video covers Agda's syntax, propositions as types, and functions, including the concept of propositions as types, uninhabited and inhabited types, bottom and top, and dependent functions. Muricy also discusses type-safe subtraction, vectors, the sigma type, and dependent products. The presentation concludes with a discussion on constructing and deconstructing matrices using Haskell and Agda, and the use of pragmas and postulates to interface with Haskell code and create functions.

Outline: • Syntax (defining types, functions etc) • Simple proofs • Simple programming • Dependently typed programming (sigma and pi types)

Does God Code in Haskell?

Professor and accomplished programming language researcher Philip Wadler believes that typed lambda calculus was discovered not invented – part of the underpinnings of the universe itself. As a result, functional programming languages are more fundamental and deeply justified than their alternatives.

We talk about this principle, which has guided his career. Phil takes us through the history of computer science from Turing to Alonzo Church. Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in.

This guy never ceases to amaze me.

I removed the protective glass from a CMOS image sensor, and used optical immersion oil to couple the bare image sensor to a 40X NA=1.3 microscope objective.

Joe Armstrong (RIP) is one of the inventors of Erlang. When at the Ericsson computer science lab in 1986, he was part of the team who designed and implemented the first version of Erlang. He has written several Erlang books including Programming Erlang Software for a Concurrent World. Joe has a PhD in computer science from the Royal Institute of Technology in Stockholm, Sweden.

The video that got me into engine build videos.

In this talk Simon discusses Haskell’s birth and evolution, including some of the research and engineering challenges he faced in design and implementation. Focusing particularly on the ideas that have turned out, in retrospect, to be most important and influential, as well as sketching some current developments and making some wild guesses about the future.

I watched this years ago. Dude is Very New England. :)

• WatchEyes
• Cutting Edge Engineering
• Martin Doolaard
• Clickspring
• 3Blue1Brown
• The Signal Path
• Democracy Now
• Tech Ingredients
• Applied Science
• Cody’s Lab
• NileRed
• Fireship
• Mental Outlaw
• Behind the Bastards
• Two Minute Papers
• bigclivedotcom
• Hackaday
• The Amp Hour
• Andreas Spiess
• Tsoding
• No Boilerplate
• CinemaStix
• Pitching Ninja
• Jeff Geerling
• Strange Loop Conference
• Impure Pics
• Psionic Audio
• Computerphile
• Abom79
• Tweag
• Serokell
• NixCon
• IOG Academy
• Mend It Mark
• Man Carrying Thing
• Vimjoyer

• 00:44 using Haskell, Nix, and Emacs for integrated offline development
• 08:48 building environments for particular dependencies with Nix
• 09:58 what Emacs and GHC have in common
• 12:58 developing with typed holes
• 14:43 compiling to categories
• 20:35 learning to love mathematics
• 22:41 applications for compiling to categories
• 25:25 Coq
• 28:15 specifying the ByteString library in Coq
• 34:30 Why Haskell?
• 40:00 writing a compiler in C vs Haskell
• 43:32 gitlib
• 45:52 getting your head around Haskell
• 48:23 recursion schemes/F-algebras
• 52:33 hnix

This walkthrough blew my mind.