prusti-dev
clog
prusti-dev | clog | |
---|---|---|
23 | 150 | |
1,467 | 1,425 | |
1.1% | - | |
8.5 | 9.6 | |
14 days ago | 6 days ago | |
Rust | Common Lisp | |
GNU General Public License v3.0 or later | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
prusti-dev
-
Using_Prolog_as_the_AST
> The overall goal would be to figure out classical error conditions like nill pointers deference.
> If I can figure out if a pointer will be nil in some execution branch, there is no reason why a computer cannot do the same.
Note, this is called flow-sensitive typing (also called type narrowing) and I think that typescript does it.
https://en.wikipedia.org/wiki/Flow-sensitive_typing
> I personally would see this as an human race level upgrades. Imagine feeding your code to a CI that spit back something like: "you will have a panic at line 156 when your input is > 4"
A model checker can do that!
See this
https://model-checking.github.io/kani/tutorial-kinds-of-fail...
Other techniques are also possible
https://github.com/viperproject/prusti-dev#quick-example
(Here I could link a lot of things, I just selected two Rust projects to illustrate)
This works better if you are able to provide contracts in your API that says which guarantees you provide. Alternatively, asserts are useful too.
-
Programming Languages Going Above and Beyond
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.
https://github.com/viperproject/prusti-dev
-
Trying to find a crate that allows you to constrain the value of arguments in various ways via a proc macro
This is called refinement types and prusti might be the project you saw.
-
rustc-plugin: A framework for writing plugins that integrate with the Rust compiler
But there's also a lot of exciting work around formal verification like Prusti.
-
Is there something like "super-safe" rust?
prusti
-
A plan for cybersecurity and grid safety
Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language
-
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
Wow that sounds really cool! I'm not an expert but does that mean that one day you could implement dependend types or refinement types in Rust as a crate ? I currently only know of tools like: Flux Creusot Kani Prusti
- Prusti: Static Analyzer for Rust
clog
- Embracing Common Lisp in the Modern World
-
Use any web browser as GUI, with Zig in the back end and HTML5 in the front end
Reminds me of the approach of CLOG (Common Lisp Omnificent Gui[1]) and its ancestor GNOGA (The GNU Omnificent GUI for Ada[2]).
They also integrate basic components and even graphical UI editor (at least for CLOG), so you can essentially develop the whole thing from inside CL or Ada
[1] https://github.com/rabbibotton/clog
[2] https://github.com/alire-project/gnoga
-
Common Lisp: An Interactive Approach (1992) [pdf]
For me David Botton [0] with his work including code, support and videos is doing very nice work in this direction.
I use SBCL for everything but work because I cannot get; we are getting there, but like you say, it’s such a nice experience working interactively building fast that it is magic and it’s painful returning to my daily work of Python and typescript/react. It feels like a waste of time/life, really.
[0] https://github.com/rabbibotton/clog
- CLOG - The Common Lisp Omnificent GUI
- Clog The Common Lisp Omnificent GUI
- Clog – The Common Lisp Omnificent GUI
- Tkinter Designer: Quickly Turn Figma Design to Python Tkinter GUI
-
Want to learn lisp?
I was following along on the Windows page and didn't check back on the main README to see if any of the other instructions would help.
-
All Web frontend lisp projects
It the answer is "latter", then you could look at Common Lisp and Reblocks (https://40ants.com/reblocks/) or CLOG (https://github.com/rabbibotton/clog).
-
How to Understand and Use Common Lisp
I haven't used Clojure professionally in 10 years so with a grain of salt here are my thoughts as only one other person answered...
CL over Clojure: it's the OG Lisp that the creator of Clojure used and wanted to continue using but faced too much resistance from management afraid of anything not-Java/not-Oracle, or not-CLR/not-Microsoft, etc. Clojure shipped originally as "just another jar" so devs could "sneak" it in. If you don't have such a management restriction, why Clojure? If you want to integrate CL with the JVM, you can use the ABCL implementation, there's also something from one of the proprietary Lisps. Some useful CL features that are nice in this domain: conditions and restarts mentioned in a sibling comment (very nice to help interactively develop/debug e.g. a selenium webdriver test), ability to easily compile an exe (perhaps useful for microservices, or just to keep your deployment environment clean and not having to care about Lisp), and ability to easily ship with an open local socket allowing you to SSH in (or SSH port forward) and debug/fix/poke around in production (JVM of course lets you attach debuggers to a running process, even certain billion+ dollar companies will have supervised/limited prod debugging sessions for various hairy cases, but it's not as interactive). You should never hear CL advocates claim you can't scale to large teams/groups of engineers or large multi-million-lines sized projects, though you might oddly hear Clojure advocates sometimes claim you can't (and shouldn't) scale to such large projects -- large groups of engineers are a non-issue for them as well though, the challenge is in hiring, not in the language somehow making it impossible to modularize and keep people from stepping on each other.
Clojure over CL: its integration with the JVM is nicer than ABCL's, so if you do actually want a lot of the great world of Java stuff, it's easier to get at. Database integration libraries are better. Access to libs (Clojure or Java) is via Maven, so it's a larger ecosystem with more self-integrating components (especially around monitoring/metrics) than what's available for Lisp via Quicklisp. Clojure is very opinionated, much of it quite tasteful, and that gives the whole ecosystem a certain consistency. (You can have immutable data structures in CL, you can if you want use [] for literal vectors and make them syntactically important e.g. in let bindings, but not everyone will be on board.) Even though its popularity seems to have stopped growing, at least at the same rate as e.g. Go which it was keeping pace with for a while, it's still popular enough with a bigger community; as a proxy measure there are multiple conferences around the world and good talks at adjacent conferences, whereas Lisp mostly just has one conference in Europe per year and only occasional branching outside of that.
If you're doing a client-side-heavy webapp, ClojureScript is still amazing, CL's answers there aren't very compelling with the exception of CLOG (https://github.com/rabbibotton/clog) which takes an entirely different direction than the usual idea of translating/running Lisp on top of JavaScript and its popular frameworks.
What are some alternatives?
MIRAI - Rust mid-level IR Abstract Interpreter
kandria - A post-apocalyptic actionRPG. Now on Steam!
kani - Kani Rust Verifier
stumpwm - The Stump Window Manager
Rudra - Rust Memory Safety & Undefined Behavior Detection
awesome-cl - A curated list of awesome Common Lisp frameworks, libraries and other shiny stuff.
automem - C++-style automatic memory management smart pointers for D
electron-sbcl-sqlite - A simple boilerplate that builds an Electron app with SBCL and SQLite3 embedded
tectonic - A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
weblocks - This fork was created to experiment with some refactorings. They are collected in branch "reblocks".
rust - Empowering everyone to build reliable and efficient software.
kons-9 - Common Lisp 3D Graphics Project