4 ms·
"Democratize formal software verification [...] perfect software." Okay. I like Forth too, but that's laying it on a tad thick, imo.
by adenozine 5y ago
"Democratize formal software verification [...] perfect software."
Okay.
I like Forth too, but that's laying it on a tad thick, imo.
- smaddox 5y agoThe formal verification aspect doesn't really have anything to do with Forth, but I do expect the multistack concatentive calculus to be much more ergonomic than applicative languages for linearity, which will play an important role in formal verification. We'll have to see how it all plays out, though. But that's my goal. I'm not really interested in writing just another programming language. Even if I fail miserably, hopefully breaking the work up into small pieces and publishing as I go will at least inspire others with similar goals.
- MaxBarraclough 5y agoFormal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software, though (that's the term the AdaCore folks use). There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada. [0] https://github.com/zetzit/zz https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny