graphical programming

Stream: general

[Kendall Frey]

I've been doing some graphical programming in Lean, and I was told it would be of interest to you here. Yesterday I created an interactive 15 puzzle.

This is done in Lean with system.io, and a separate application in C# that accepts drawing commands via stdin. This way, Lean doesn't need to implement any window management, and supporting stdio is all that is required for Lean (or any other language) to create graphical applications.

3cd189ab-26e3-42d6-8a5b-b5647a606597.gif

[Kevin Buzzard]

@Markus Himmel used widgets in an ingenious way to make Sudoku in Lean as well:

https://github.com/TwoFX/sudoku

(someone was live streaming this on the Discord recently).

Anything which takes Lean out of the

a b c : ℕ,
divac : a ∣ c,
m : ℕ,
hm : b = a * m
⊢ a ∣ b + c

view and into something which looks graphical is I think great for advertising purposes. There are a couple of other projects in the pipeline as well.

[Mario Carneiro]

How about a button once you've solved the puzzle to get a lean proof that the puzzle is solvable?

[Kevin Buzzard]

With Sudoku the user manipulates the board by actually writing the Lean proof.

[Bryan Gin-ge Chen]

These look great! Is your discord the best place to keep track of these projects?

[Kevin Buzzard]

I don't really want this to be the case, that's why I was encouraging people to post here.

[Chris Hughes]

Mario Carneiro said:

How about a button once you've solved the puzzle to get a lean proof that the puzzle is solvable?

Markus's game obliges you to prove the solution is unique as well.