Next meeting on Wednesday July 24th

[Erik de Castro Lopo]

Hi all,

The next meeting will be help on Wednesday July 24th.

This month we have two talks:

Geoff Huntley : Watch me format my wife's computer

Amos Robinson : Program-Carrying Proofs in Coq: using tactics for
dependently typed programming

Abstracts below.

The RSVP is here:

https://www.meetup.com/FP-Syd/events/vcqlmpyzkbgc/

Doors open at 6pm, meeting proper starts at 6:30.

Everybody who intends to show up on the night shoud RSVP ASAP to allow our
hosts Atlassian to sort out the catering. People who said they were
going but now find that they can't should likewise update their status.

Cheers,
Erik

# Watch me format my wife's computer

Come heckle me whilst I install Linux on my wife's computer live on stage.
You'll learn all about the functional declarative operating system called
NixOS and leave questioning why your team and the industry went all in with
Docker.

If /usr/bin and /bin didn't exist what potential could that unlock? What if
ansible, chef and puppet were built into the operating system but better?
What if you didn't need to use sudo because you can side-by-side install
everything? What if it was /impossible/ to permanently break your operating
system?

NixOS is one of the most popular opensource projects on GitHub but you've
probably never heard of it. No experience with Linux or operating systems
is required. I really will be formatting my wife's computer in this session
for your entertainment and to teach you what I wish I had of known when I
first discovered Nix.

# Program-Carrying Proofs in Coq: using tactics for dependently
typed programming

Abstract:
If you’ve ever tried to write a dependently typed program in Coq, you’ve
probably been frustrated by the general difficulty of it all. The type
errors are questionable, and even if you succeed, your resulting program
barely resembles your original intent. In fact, the whole ordeal has
probably put you off dependent types for good. But we must persevere.

While Coq’s support for dependently typed programming is pretty terrible,
its support for dependently typed proving is second-to-some. Coq’s tactic
language is really all about construct dependently typed proof terms - so
why can’t we use tactics to construct dependently typed program terms?
Let’s find out.

--
----------------------------------------------------------------------
Erik de Castro Lopo
http://www.mega-nerd.com/