syntheticblue project notes
╭
𝟙𝟡·
I planned one project, ‘Sudoku by Proof’, before I discovered Lean Sudoku. A simple logic language I'm working on, Sapphire, instead - although I plan to generate
𝔽
┊
𝟚𝟞·
I'm easily distracted when programming by potential improvements to my ‘ecosystem’ (a friend put it nicely: “you're a tools guy”). I dogfed (dogfooded?) my Python and
𝕖
┊
C preprocessor to itself for the first time in a while and, well, it took the afternoon. ‘Zypp’ does really important things, like replacing some operators with more
𝕓
┊
math-y versions available in Unicode: ‘&&’ in C and ‘and’ in Python both get replaced with ‘∧’, which I use in my syntax for logical formulae I call ‘Sapphire’. I
┊
like minimalist punctuation and Python's visible block structure, so, among other less-critical things, Zypp inserts curly braces into my C code. Currently it's a
┊
total hack and gets changes and fixes constantly as I write new code - eventually I plan to create a parser and I'll more legitimately describe the code I write as
╰
‘Midnight’ (the dynamic language formerly known as ‘hacked up Python’) and ‘Cobalt’ (the compiled language formerly known as ‘really broken C’).
𝟯
/
𝟘𝟞·
When Peano's axioms are constrained to first order Logic, the Natural numbers cannot be defined precisely - they admit the interesting structure of non-standard
┊
arithmetic. But it's time to learn a bit about Reverse Mathematics, which works with second order Logic because, while the expressiveness has its burdens, feels
┊
non-negotiable.
𝟰
/
𝟘𝟠·
Hello World in the Spectrum languages Sapphire, Midnight and Cobalt. I added some fancy features to the empty Spectrum file I had posted, implementing solutions to
┊
that challenging problem Computer Science students usually don't see until 2nd or 3rd year!
╰
𝟚𝟛·
A puzzle project coming together:
