Show HN: The Logos Programming Language and Theorem Prover(logicaffeine.com)

3 pointsby tristenharril y a 6 mois3 comments

Show HN: The Logos Programming Language and Theorem Prover

https://logicaffeine.com/crates

3 comments

3 days of refactoring, over 140,000 lines of code touched. All ~2500+ tests still passing. I'm going to sleep! Another all-nighter. Talk about a fun Friday night! :) I frickin love this stuff so much! It's like having an ARMY. A LITERAL ARMY OF PHD's. You can raise mountains in minutes it feels like. That's been my experience. You all may call it slop, but I think spec driven development is great. I just think that if you have to write documentation to explain the code, then either your language syntax isn't precise and easy enough to understand, or you are doing something convoluted and potentially stupid. It's a language surface problem. The languages of the past were constrained by human limitations. In the past you'd be out of your mind trying to write a crazy multi-pass compiler and doing all the tips and tricks to make something fast because a human had to maintain it. If you formally specify the constraints of something, design tests that codify those constraints, and then develop code that passes those tests without cheating or changing them, then these new technologies rapidly gain something that gets much closer to determinism.

I think for me the key thing has been treating the tests like I'd treat my foundation. When something is wrong, or I need to design something, it starts with a spec that tries to solve the domain problems, which turns into a plan for tests that will fail when we run them now, but should pass when we have completed the implementation. You may miss edge cases, but when you identify them, you fix them for good by adding tests for them.

One of the tricky parts is creating a good test harness. You have to have a great harness and I need to go through and improve mine!

Anyways, I'm exhausted folks, pizza is all gone and the mountain dew ran out. Time for me to snooze.

tristenharril y a 6 mois

Creates: https://crates.io/crates/logicaffeine-base https://crates.io/crates/logicaffeine-data https://crates.io/crates/logicaffeine-kernel https://crates.io/crates/logicaffeine-lexicon https://crates.io/crates/logicaffeine-system https://crates.io/crates/logicaffeine-proof https://crates.io/crates/logicaffeine-language https://crates.io/crates/logicaffeine-compile https://crates.io/crates/logicaffeine-cli

Documentation: https://docs.logicaffeine.com Studio Example: https://logicaffeine.com/studio?file=examples/code/memory/zo...

tristenharril y a 6 mois

Enhancements Short Term Roadmap -> https://github.com/Brahmastra-Labs/logicaffeine/issues?q=is%...