I'm an experienced java enterprise developer but new to Rust. I've taken a stab at building a predicate logic tautology prover for formal constructs at GitHub - glancey/axiom · GitHub, and welcome suggestions and comments.
My goal is to create a full-fledged inductive logic programming (ILP) AI solution in Rust. A more modest objective is to incorporate my prover in constructing games that can be algorithmically solved, or not (respecting Godel's incompleteness).
It would be nice to let people know, both here and in your README, that you vibe coded this via Claude. Some people (myself included) are less likely to want to do a code review on AI-generated code, for a number of reasons. And being honest about the source of your code is vital if you intend for this to be used by others.
In general, I discourage advertising vibe-coded projects. But if you are going to, please be honest about it.
My apology for not disclosing that. My intent was to get comments on the code, based on my instructions on what to construct. I mainly used Claude to see how accurately it could compose Rust syntax and to see how effectively it could analyze complex algorithms, not to create functionality out of whole cloth.
The entire structure of the application and functional details are all mine.
Lest you think your time could be better spent on pure code - completely manually written - I trust you understand that most applications moving forward will be AI written, and by designers who know little or nothing about the underlying syntax.
Glenn
I appreciate the intent, and I understand the desire to experiment with AI, especially as I've heard plenty of good things about Claude. However, I don't see why it's more worth my time to do a code review on AI-generated code just because there will be more such code in the near future. On the contrary, an abundance of worthwhile AI-generated code tells me that I needn't apply myself to anything in programming, since AI can do it at least as well as me.
In my opinion, there are only two possible futures as far as AI devs are concerned:
AI will take over writing applications, and human "programming" will become just another low-effort low-cost callcenter-style job, where we just vaguely supervise models churning out code. Personal development will descend to merely asking Claude to generate the code for you.
In this scenario, there will be little reason for anyone to use dependencies, because anything the AI needs it can write itself just as well. If you anticipate such a world, it seems curious to develop applications for other people, when they could have generated it just as easily as you did.
The AI market will collapse under the weight of its own failed promises, leaving few companies actively chasing AI-powered application development. We will still use AI models for certain things, but far from the world pictured in #1. Except for a lot of software developers suddenly losing their jobs, nothing much happens in the ecosystem - it just goes back to what it was a few years ago.
I personally think #2 is far more likely, but if you disagree, that's fine. I just can't see a world in which AI will take over programming, but humans still care. Either way, I tend to stay away from AI in programming, and advise others to as well.
I understand your concerns. But I don’t think either scenario 1 or 2 is accurate.
I retired from programming last year after more than 40 years on the job. I loved every minute of it, the challenge, the beauty of creating out of a few lines of code. But since I left my last option, I doubt few of my colleagues are still on the job. Agentic coding has flooded in.
My take now, after working with Claude for just a few weeks , is that programming won’t disappear. It will just take on a new form. Adoption isn’t surrender. That doesn’t mean all is well. It never really is.
Coding over the years was becoming more mechanical. Decision making was taken out of the programmer’s hands and left to project managers , scrum masters and an alphabet soup of DevOps. Yuk!
AI is our revenge.
Glenn
I builded the project. Tried it out> ,➜ release git:(main) ./axiom validate "f(a, b, c)"
Select type to validate against:
- individual_variable
- logical_symbol
- operation_symbol
- individual_constant
- relation_symbol
- term
2
Error: not a valid logical symbol: f(a, b, c)
I wanted to help you out with it, but there is no way im going to read the chunks of code without me getting a headache. Please add some docs! And I think it's very usable, also when i ran the validate then it threw me many errors, please don't display the options (you can try validate them before rendering).
Thanks, hi-sam, for getting in touch. Axiom is a work in progress and user input like yours is appreciated and needed. Based on your comments, I added a function to normalize logical symbols:
/// Normalizes a natural-language logical symbol name into its symbol form.
/// Returns the mapped symbol string, or the original input if no mapping matches.
fn normalize_logical_symbol(s: &str) -> &str {
match s.trim() {
"and" => "\u{2227}",
"or" => "\u{2228}",
"implies" => "=>",
"not" => "\u{00AC}",
"iff" => "<=>",
"for all" => "\u{2200}",
"there exists" => "\u{018E}",
"equals" => "==",
other => other, }}
Now, when you can enter ./axiom validate “and”, you get the result:
(base) glennsilverman@mac debug % ./axiom validate "and"
Select type to validate against:
- individual_variable
- logical_symbol
- operation_symbol
- individual_constant
- relation_symbol
- term
2
logical_symbol(∧)
The command, ./axiom glossary, returns documentation on the validation options. There’s ./axiom –help, which gives you the available commands. You can also run cargo docs and get extensive documentation on the application. The code, itself, is heavily commented. I’m more than happy to walk you or anyone interested in the code through it to understand it and better grasp my vision. Again, thanks for your interest.
Glenn
Hi-sam,
To expand further on your comments, the purpose of the options menu when you enter a validate command is to allow extensive testing on the each of the language constructs. I want to guarantee that the code is sufficient to only accept valid constructs so that the command, ./axiom tautological-proof works as intended:
./axiom tautological-proof "not(P and Q) => (notP or notQ)"
Formula to prove: (¬(P and Q) => (¬P or ¬Q))
Tautology: not(P and Q) => (notP or notQ)
If the designer who generated the code doesn't understand the language syntax, it would be very unreasonable for them to ask others, particularly in this forum, to review the code manually. So the scenario you're describing is not applicable to this conversation.
I get your point. But to be clear, I understand the code and the syntax. I don’t need to manually write all the code. But none of that means the code is not without bugs. Nor does it imply that it’s the most efficient. I suppose all the code you write is always bug free and is never subject to improvement. I’m certainly not asking you or anyone to waste time on things that don’t interest them.
I was replying to your statement about people generating code who do not understand the syntax. I realize you are not one of those people.
One other point, and maybe you are right that this is the wrong forum on this but I’ve always understood code review to be more than just about syntax and algorithmic efficiency, but also about concept. Is the application and its parts conceptually correct based on the purpose for which it was designed? Creating a logical theorem prover is a complex subject and not at all straight forward.
I posted on this forum to solicit comments and suggestions not just about code but to get others with the requisite domain knowledge to chime in.