PS1: Functional Programming

[bennn]

Write a first problem set: intro to Coq + FP. I think we can avoid proofs entirely.

Decide which libraries should be available.

[bkc39]

What's they syllabus here bruh? How hard do we want to follow the 3110 PSets?

[bkc39]

Also, I don't think we should avoid proofs. Things like refl, simpl and rewrite can be introduced at this stage with no additional pain. It's also a good way to step through the evaluation model.

[bkc39]

After thinking about it I think that maybe a simple game where the core logic is implemented using higher order functions might be the right thing to do here. We could link against a GUI written in OCaml or something. Basically, the lecture schedule we seem to be converging on in #10 seems VERY abstract at the beginning compared to the current version of CS 3110 so I think we should counterbalance by a more "real world" first problem set. It will help convince people that this isn't all just abstract nonsense.

[bennn]

That's hardcore. I fear GUIs. But ok. How about an alarm clock app? Design a datatype for a 24-hour clock (could use sum types, integers, dependently-typed integers, ...) and implement an API for our GUI.

My plan for ps1 was practice with types. Have a few 3110-style type/expression problems, and make the coding follow a pattern of:

1. design a type
2. write a function, first thinking about what it should do
3. informally argue your function's correctness (i.e. unit test)

Like, design a type for binary numbers / polynomials, write some functions and examples. We could also do roman numerals, etc.

[bkc39]

I would like to in general do more interesting problem sets than 3110. I was thinking of doing a terminal based game of Tic-Tac-Toe. The assignment would consist of

• Basic Types and Proofs
• Curry howard based exercises.
  • Here is proof, what is the program?
  • Here is the program what is the proof?
• Formally verified printf
• Tic-Tac-Toe game
  • Uses the printf function above
  • Prove that the the implementation will never lose.
  • I envision a fill in the missing parts of the proof type exercise.
  • We do all the user input parsing, etc.

[bkc39]

In general though, I think I'm more of a supporter of "argue informally, and then translate that into a proof", then just "argue informally". But I think in general I feel like proofs should play a much more central role at the beginning than you are. My fear is that the jump in proof complexity will be too high between the first and second problem sets.