F*: A general-purpose proof-oriented programming language

5 comments

• cyanregiment 1 hour ago
  Clicked like 5 pages and never found 1 code example.

  Idk why languages don't have their syntax in a sandbox front-and-center on the home page.

  It's like a video game site with zero screenshots or videos (also rampant).

  New programming languages I want 2 things:

  1. What does the syntax look like

  2. Why would I use this language

  Talk about the proof logic, show the syntax, thank you

  [-]
  • rixed 49 minutes ago
    I'm the opposite: when landing in a programming language site I want to know the user case the authors had in mind, the memory model, the type system, the compilation targets, the data layout, the control structures, and only at the end just check that the syntax is not indentation based.
    [-]
    • sroerick 27 minutes ago
      So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?
      [-]
      • zlsa 17 minutes ago
        I think this falls under "[wanting] to know the user case the authors had in mind"
      • rustfreeforme 24 minutes ago
        That seems to be what he just said.
  • munchler 1 hour ago
    https://fstar-lang.org/tutorial/
    [-]
    • aleph_minus_one 1 hour ago
      > https://fstar-lang.org/tutorial/

      FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

      > https://fstar-lang.org/index.html#learn (1)

      and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

      In the section of (1) also the PDF version is linked:

      > https://fstar-lang.org/tutorial/proof-oriented-programming-i...

      [-]
      • cyanregiment 51 minutes ago
        I still don't see any code examples!

        But I do see the editor to try it.

        I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

        It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance

        Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!
    • _flux 51 minutes ago
      I guess it's a bit popular right now

          * Error 17 at Welcome.fst(24,0-28,30):
            - Could not start SMT solver process.
            - Command: ‘/home/site/wwwroot/fstar/bin/z3’
            - Exception:
                Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
          
          1 error was reported (see above)
  • Verdex 1 hour ago
    To borrow your video game analogy. F* is the dwarf fortress of programming languages. Screenshots are only going to confuse anyone who isn't ready to take a significant mental journey.
  • rainyq 1 hour ago
    just click the screenshot
    [-]
    • cyanregiment 46 minutes ago
      Takes you to an empty editor with still no code examples
  • qzzi 1 hour ago
    I clicked on 2 links on the main page in the Learn F* section...
    [-]
• pvsnp 1 hour ago
  I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
• IshKebab 9 minutes ago
  F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out.

  Does it get basic stuff like subtraction and u8 right, unlike Lean?
• kirlfiend_grill 58 minutes ago
  > F* (pronounced F star)

  No, it isn't.

  [-]
  • rustfreeforme 23 minutes ago
    "Now introducing my new language, FFUUUUU--. It's a fork of Rust."
• 3lambda 30 minutes ago
  [dead]