3 ms·
TIL... I didn't realise that Lean was usable(?) for 'actual programming' rather than just math proofs etc
by anentropic 1y ago
TIL... I didn't realise that Lean was usable(?) for 'actual programming' rather than just math proofs etc
- gopiandcode 1y agooh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs. Things like: - bindings to godot (https://github.com/kiranandcode/lean4-godot https://github.com/kiranandcode/lean4-godot) - advent of code (https://github.com/kiranandcode/lean-aoc https://github.com/kiranandcode/lean-aoc) - ffi bindings to constraint solvers (https://github.com/kiranandcode/cleango/ https://github.com/kiranandcode/cleango/) Obviously a slightly biased selection here, but the key point is to clarify that it's more than feasible to use it for real programs that do all sorts of non-mathy stuff.
- anentropic 1y agoGodot games in Lean sounds wild...!