I love this guy’s style of iteration. A truly talented mechanical engineer.

This guy always does a really great job. I love that he doesn’t ramble in my ear the whole time.

I’ve learned so much about welding, machining, boring, hydraulics, and most of all: doing things the right way quickly from this channel. Abom79 used to scratch this itch and I do sometimes watch his channel but for some reason, this is even more entertaining.

This is a beautiful quote from David.

I might not appreciate his films (even after having gone to an avant garde art school) but the perspective that he so articulately described here illustrates the true catharsis of human experience that I can only hope to dance around metaphorically.

The video that got me into engine build videos.

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)

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

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.