F* – A Proof-Oriented Programming Language

Post by debugnik » Thu, May 16, 2024, 3:28 PM UTC

seanw444 wrote: post #15

pelagicAustral wrote: post #7

The first thing that came to mind when I entered the site was the resemblance of the classic Soviet iconography to their logo, sans the hammer and sickle, then I checked the repo, and coincidentally, they have a recent commit (`c6fac4d`) titled " kremlin -> karamel " [0] ( [...] a tool for extracting low-level F programs to readable C code*)... Apparently, the commit is one big rename operation from Kremlin to Karame…

I'm curious why the resemblance and homage to the Soviet Union in the first place, but I find it sad that people feel the need to rebrand things like this, to avoid the mob. Just because I don't like communism, doesn't mean people can't have things named after one of recent history's most well-known superpowers, with admittedly cool style.

Post by Jtsummers » Thu, May 16, 2024, 3:36 PM UTC

letmeinhere wrote: post #10

eggy wrote: post #5

I prefer F#/F* syntax, but I had to go with Ada/SPARK2014 for the safety-related control systems I am trying to verify formally and use for high-integrity applications. Rust is making some inroads with AdaCore and Ferrous Systems partnering on providing formal verification tools for Rust like they do for Ada/SPARK2014, but Rust still doesn't have a published standard like C, Common Lisp, Prolog, Fortran, COBOL, etc.…

My understanding is that the key feature of SPARK is design-by-contract aka run-time enforced pre- and post-conditions plus invariants for loops. Whereas F* lets you define dependendent types, a subset of which are compile-time constraints similar to those SPARK contracts. Is that a fair contrast?

Post by ykonstant » Thu, May 16, 2024, 3:45 PM UTC

jfoutz wrote: post #4

tombert wrote: post #2

Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…

Lately I've been dabbling with lean. pretty tight vs code integration. I don't know why I keep getting pulled toward dependent types, like a damn moth to a flame. I get a little scorched, then, oh I should try ... But yeah, compiler checked properties are something kinda magical. Even more when you can specify the property to check.

Post by tombert » Thu, May 16, 2024, 3:55 PM UTC

lambdanik wrote: post #16

tombert wrote: post #2

Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…

Have you seen https://github.com/FStarLang/fstar-vscode-assistant ? Copilot & F* works pretty nicely. We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el

Post by samueldurante » Thu, May 16, 2024, 3:58 PM UTC

bmitc wrote: post #27

I've never understood the relationship between F# and F*. I had previously come to the conclusion that F* was merely inspired by F#'s syntax and base-level semantics but that was where the relationship ends. As far as I can tell, F* is not a .NET language and doesn't run on the CLR. Is that correct? In the description it says it compiles to OCaml, which confuses me even more about the F* naming. What is the relations…