... opinions on Ada/SPARK, its relation to Rust, and why I shouldn't write an SBBS clone in Ada/SPARK. :^)
s/schumeboard/schemeboard
(dvorak master race)
You should write one!
not sure what a schemeboards mind is but i dont see the issue sbbs is already scheme making another clone in scheme is dumb maybe lipth or smalltalk would fit a schemeboards opinion better
real opinion this belongs on /sol/
maybe making sbbs more portable instead of mit scheme but thats more of a rewrite than a clone if done from scratch
>>1
Ada is essentially a somewhat more powerful and less error-prone version of Pascal, originally developed during the time period when Pascal was seen as the standard programming language and C had not yet conquered the world. Many of its improvements in that sense are just syntactic modifications, like switching from block comments to line comments and making compound statement bodies the default for control flow constructs (to prevent mistakes like Apple's "goto fail"). Then they added generics, some other stuff we take for granted today, and in some cases, features that haven't appeared in any other major language since Ada.
The base language is not opinionated about mutable or aliasable state the way some newer languages are. Mostly it just makes it cumbersome to work with references and allocations (compared to Pascal and C) and marks deallocation as an "unsafe" operation. SPARK is far more strict. It called for the addition of contract-based programming features to Ada, and uses theorem proving to programmatically verify your claims about how your code will behave. All of that is encoded in an extremely verbose notation on top of an already verbose base language. C programmers like to dismiss Rust for being verbose, and for "duplicating" the efforts of the Ada/SPARK designers, but those criticisms are both nonsense, and together they are transparently disingenuous. Rust simplifies and automates so many tasks that SPARK makes complex and manual. That's not an indictment of SPARK, though; that's just what theorem provers were like in those days.
Modern SPARK is trying to follow Rust's example and make its own memory safety capabilities more ergonomic, and the Rust developers have spent years trying to help them. I don't know how far along they are, but that's the closest connection between these languages.
As for using Ada to write forum software, I think that's absurd; far too much work. Go for it.
is automated theorem proving like pure lisps "pltp" really that difficult it came a decade before spark83s ada
another question was theorem proving ever in rusts design https://rust-formal-methods.github.io/tools.html
id say the same about ada but spark has it
and looking at 1-san i doubt he even cares about that in the comparison and in my opinion should drop the spark thing if its for le security probably pick a different language even rust like you said until the second he unsurprisingly enables rusts unsafe mode out of frustration and doesnt use any of the formal method utilities designed around rust
>>7
Most language features that have ever existed were developed in some Lisp dialect before they appeared elsewhere, but that doesn't invalidate their later appearances.
I assume >>1-kun has little to no experience with any of these languages, so I gave him the basics. You're right that SPARK is an insane choice for writing a forum. Even normal Ada demands too much ceremony for me to enjoy working with it. Maybe >>1-kun will feel differently, or maybe not.
Also, very few people are using real formal verification techniques with Rust, partly because those tools aren't mature, and partly because you can get pretty far by hacking together some primitive "proofs" using tricks like session types. However, Rust does give you a higher baseline for reasoning about mutable state when compared to stock Ada, and the borrow checker is far less difficult to work with than SPARK.
while maybe that is fallacious to invalidate later appearances ive written pascal and formalish lisp before not ada spark thus the questions
what isnt fallacious is to call out how broken and fundamentally flawed later appearances are in retrospect on site with a lisp nomenclature as comparison but pltp has its own fundamental faults too down to the implementation which is important here
im not sure who 1-san is even trying to contact >>8-chan
but i believe they wanted information on a lispish take so its a little weird to not mention something like pltp
Rust does give you a higher baseline for reasoning about mutable state when compared to stock Ada, and the borrow checker is far less difficult to work with than SPARK.
ive never even had to patch rust code yet but ill assume unsafe mode makes some of this invalid https://users.rust-lang.org/t/unsafe-rust-how-do-i-inform-the-compiler-of-side-effects/62345 but the borrow checker is still intact since ive studied the borrow checker and how it should be passive how does this compare to sparks do you have to manually write borrow checks in and play with gibberish that doesnt explain why something has wrong references
a notice for >>8-chan 1-san makes use of :^) when describing ada spark they mean to use a language related to agencies like how ada came from a dod initiative
im not sure of a "safety language" 1-san could use that "glows" but i do know unlike a majority of formal lisps usually these languages have use in real cases where complexes are getting destroyed and lifes snuffed out its much different from ivory tower trying to demonstrate something
maybe if >>8-chan is willing to be a clown today consider recommending one of those languages you can barely find traces of on the internet that is also like a lisp but doesnt have to be lisp