BFPG - March 2024 - Fennel: a Lisp that compiles to Lua / Propositions as Types

Agenda

• 18:00: Welcome and setup
• Presentation #1: Propositions as Types (Donovan Crichton)
• Presentation #2: Fennel: a Lisp that compiles to Lua (Jack Kelly)
• 20:00ish: Pack down, exit, head to Criterion pub.

Propositions as Types (Donovan Crichton)

This talk will introduce you to an alternative way to think about types and
functions. Under certain conditions your types can be logical propositions and your functions can be mathematical proofs. Proving a theorem becomes no different to writing a program in a (particular kind of) pure functional programming language. We will explore this notion in the Idris functional programming language and see examples of how proofs can be very useful to day-to-day programming.

Fennel: a Lisp that compiles to Lua (Jack Kelly)

Lua is a great language for scripting other programs, and is used all over the place from NeoVim to many games. It has pretty good semantics but some syntactic warts that make it a bit frustrating. Jack will introduce Fennel, a Lisp which compiles to Lua. Some parts of this talk will be interactive, so bring a telnet client if you have one.