syntheticblue project notes
stuff projects rants
𝟙𝟡· I started my main project, ‘Sudoku by Proof’ before I discovered Lean Sudoku. I think it'll be fun to continue anyway. I've been slowly working through “Mathematical Logic through Python”
while writing my own tools - even my own variants of programming languages! Still all a jumble, a little bit is starting to congeal and hopefully I'll make some consistent progress.
𝔽 𝟚𝟞· 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.
𝟙𝟝· To encourage myself to get more done, I'm posting a bit or two from my Symbolic Logic project. A few simple propositional proofs as things currently stand.