FStar
Giraffe
FStar | Giraffe | |
---|---|---|
42 | 19 | |
2,570 | 2,059 | |
0.6% | 0.8% | |
9.9 | 6.8 | |
5 days ago | 3 days ago | |
F* | F# | |
Apache License 2.0 | Apache License 2.0 |
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.
FStar
- Lean4 helped Terence Tao discover a small bug in his recent paper
-
The Deep Link Equating Math Proofs and Computer Programs
I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.
For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.
For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).
For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).
And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).
-
If You've Got Enough Money, It's All 'Lawful'
Don't get me wrong, there are times when Microsoft got it right the first time that was technically far superior to their competitors. Windows IOCP was theoretically capable of doing C10K as far back in 1994-95 when there wasn't any hardware support yet and UNIX world was bickering over how to do asynchronous I/O. Years later POSIX came up with select which was a shoddy little shit in comparison. Linux caved in finally only as recently as 2019 and implemented io_uring. Microsoft research has contributed some very interesting things to computer science like Z3 SAT solver and in collaboration with INRIA made languages like F* and Low* for formal specification and verification. But all this dwarfs in comparison to all the harm they did.
-
What are the current hot topics in type theory and static analysis?
Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.
-
Why is there no simple C-like functional programming language?
F* is a dependently typed language that can be transpiled to idiomatic C via the KReMLin compiler. It’s very ML-ish to write and you can leave out some proofs. It also has the benefit of being used to write a formally verified TLS implementation that’s in wide use throughout industry.
-
[Media] Genetic algorithm simulation - Smart rockets (code link in comments)
As I said, dependent types attempt to solve this problem. F* is a language where you can express complex logic as a type. The catch is, these types are checked by an SMT solver. If the solver can satisfy the type checking, then great, and you move on. If it can’t, you have no idea why, and either have to guess or manually write the proof anyway. Contrast this with Standard ML which has a proof of the soundness of its type system.
-
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
So kind of like F*? https://www.fstar-lang.org/
-
old languages compilers
F*
-
Pegasus spyware was used to hack reporters’ phones. I’m suing its creators; When you’re infected by Pegasus, spies effectively hold a clone of your phone – we’re fighting back.
Nevermind that academia has come up with far safer ways to do a few things but social norms & inertia prevent their wider adoption (well okay, it also has a barrier to entry in the education required to use it but I don't think someone with the knowledge to meaningfully contribute to an OS kernel can be considered uneducated nor unable to learn).
-
[Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use
Maybe that's a little off topic here, but if you like fixing bugs, i suspect you might also enjoy showing that there are no bugs at all. Check out languages like F* https://www.fstar-lang.org/ It's a proof-oriented programming language. You can use it to write code that has no bugs at all. And you once you're done, can convert F* to C or other languages.
Giraffe
-
The combined power of F# and C#
Giraffe is another interesting one to explore: https://giraffe.wiki/
Giraffe is nice because it is itself built "just" as ASP.NET Core Middleware so it plays a bit more nicely than Suave with a mixed stack of C#-defined Middleware.
It's more likely you accidentally fall back into just translating C# patterns to non-idiomatic F# with Giraffe, but it's also nicer when in that case of needing to live in both worlds and use a mixture of libraries built for C# ASP.NET projects.
-
ASP.NET Core updates in .NET 8 Preview 4 - .NET Blog
There are also some F# frameworks built on top of ASP.NET core like https://giraffe.wiki
- Confusion in learning Giraffe's HttpHandler
-
Is there any advantage to using F# instead of C#?
If you have an interest in F#, I highly recommend diving in because (1) it has a ton of things you might learn to appreciate in C#; (2) it has things C# cannot have. I do like some of the suggestions people have made regarding mixing your code bases, but I'll also say that building, say, endpoint routing in Giraffe is (to repeat myself) easy, simple, and elegant.
-
Targeting Node, Bun and Deno With F#
Bix is a micro-framework designed with F# in mind and that runs on both Deno and Bun! and in theory it also should even run in a service worker! (intercepting fetch requests) although I haven't tested that yet, it offers a general purpose handler that coupled with a set of route definitions it can bring a Giraffe/Saturn like framework to life in JavaScript runtimes which is incredibly awesome! useful? maybe not 😅, but awesome indeed. Let's see some code for it
-
If you were to create a Web API today from scratch how would you do it ?
Backend: Most likely it would be a toss between https://saturnframework.org or https://giraffe.wiki. They both combins the extremely good type system in F# combined with the ease of a minimal API.
-
Is it possible to run C# asp.net core MVC and f# giraffe in a single solution
I was wondering if its possible to simultaneously run a C# core MVC project in combination with https://github.com/giraffe-fsharp/Giraffe
-
Overriding JSON serializer in Giraffe
By default Giraffe, the framework which I use as a web server, uses Newtonsoft.Json to serialize results to JSON. However, for discriminated union, it generates quite a lot of JSON so I've switched to System.Text.Json which is built into newer versions of .Net Core. In combination with FSharp.SystemTextJson package allows serializing discriminated unions more gracefully. All we need is to decorate Branch type with JsonFSharpConverter(JsonUnionEncoding.BareFieldlessTags) attribute.
-
Introducing Giraffe.Htmx
Giraffe is a library that sits atop ASP.NET Core and allows developers to build web applications in a functional style; dotnet new giraffe is literally my starting point when I begin a new web application project. (Rather than write three more sentences filled with effusive praise, I’ll just leave it at that; it’s great.) It also provides a view engine (that builds upon Suave‘s “experimental” view engine) which uses an F# DSL to define HTML in a strongly-typed way. It has been incredibly efficient for a while, but with .NET’s work over the past two releases at improving performance, and Giraffe’s adoption of those techniques, it is lightning fast.
-
Show HN: F# web server in 3-4 lines of code
Wrapping ASP.NET Core to be easier and more idiomatic with F# seems to be a common domain. Out of curiosity, did you look at any existing projects? If so, what was lacking from them that made you decide to write WebFrame?
Giraffe: https://github.com/giraffe-fsharp/Giraffe
What are some alternatives?
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Suave.IO - Suave is a simple web development F# library providing a lightweight web server and a set of combinators to manipulate route flow and task composition.
lean - Lean Theorem Prover
Saturn - Opinionated, web development framework for F# which implements the server-side, functional MVC pattern
dafny - Dafny is a verification-aware programming language
ASP.NET Core - ASP.NET Core is a cross-platform .NET framework for building modern cloud-based web applications on Windows, Mac, or Linux.
koka - Koka language compiler and interpreter
Falco - A toolkit for building fast and functional-first web applications using F#.
VisualFSharp - The F# compiler, F# core library, F# language service, and F# tooling integration for Visual Studio
ASP.NET MVC
stepmania - Advanced rhythm game for Windows, Linux and OS X. Designed for both home and arcade use.
Freya - Freya Web Stack - Meta-Package