Zulip Chat Archive

Stream: general

Topic: graphical programming


view this post on Zulip Kendall Frey (Jul 26 2020 at 12:49):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 12:58):

@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.

view this post on Zulip Mario Carneiro (Jul 26 2020 at 13:05):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 13:10):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 14:38):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 14:48):

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

view this post on Zulip Chris Hughes (Jul 26 2020 at 19:44):

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.


Last updated: May 08 2021 at 18:17 UTC