4 ms·
F*: A general-purpose proof-oriented programming language
- pvsnp 2mo agoI liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
- rixed 2mo agoWhat do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?
- aw1621107 2mo agoI think it's meant to be parsed as "I liked being able to (express (calling external libraries))", not "I liked being able to (express calling) (external libraries)"
- pvsnp 2mo agoYes. Probably could’ve written it better but I’ve not poked around F* in a while and I was writing on my phone. Say you’re calling an external function implementation in hardware, being able to express those interfaces as external makes it viable to use F* vs assuming everything is open source and introspectable.
- cyanregiment 2mo agoClicked 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
- rainyq 2mo agojust click the screenshot
- cyanregiment 2mo agoTakes you to an empty editor with still no code examples
- qzzi 2mo agoI clicked on 2 links on the main page in the Learn F* section...
- deleted 2mo ago[deleted]
- munchler 2mo agohttps://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
- aleph_minus_one 2mo ago> https://fstar-lang.org/tutorial/ 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 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-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i...
- cyanregiment 2mo agoI 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!
- kirlfiend_grill 2mo ago[flagged]
- aleph_minus_one 2mo ago> > F* (pronounced F star) > No, it isn't. https://fstar-lang.org/ https://fstar-lang.org/ claims otherwise: "F* (pronounced F star)".
- 3lambda 2mo agoWould this language be useful for implementing compilers and formally proving things about them?
- physPop 2mo agoyes thats the main reason, agda , coq similar ideas
- dnautics 2mo agopersonally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.
- nickpsecurity 2mo agoThey started out that way. Keeping consistency between the formal specification and the code was always difficult. The further apart they are in distance or notation, the more difficult it is. So, the field experimented with verificatiom-oriented languages to localize changes.
- _thejanus_ 2mo agoWhat do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this. Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly
- _thejanus_ 2mo agoI think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive enough that your source language can be pretty wild with your denotational semantics. Grain of salt though, because I haven’t tried this concept in anger at all
- rustfreeforme 2mo ago[dead]
- rustfreeforme 2mo ago[dead]
- IshKebab 2mo agoF* 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?
- gugagore 2mo agohttps://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
- IshKebab 2mo ago> But it doesn’t lead to confusion when doing mathematics in a theorem prover. This is demonstrably untrue. In any case that post is pretty unpersuasive. Basically saying it's too tedious to do it right, in a language whose whole purpose is tediously doing things right! Probably the better conclusion is that more proof automation is needed for simple things like "this number is not negative" so it is less tedious. (I'm not a Lean expert but I was totally put off by it happily accept a uint8 with value 300.)
- yourewrongsorry 2mo ago[flagged]
- boutell 2mo agoI guess responsive stylesheets can't be implemented without side effects...
- LelouBil 2mo agoI like Haskell, and to me this seems really useful as a kind of "noob" to functional languages. Is this used in the industry ? And for what kind of software ?
- LelouBil 2mo agoI found these links in the F* book https://www.microsoft.com/en-us/research/blog/everparse-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/ https://www.microsoft.com/en-us/research/blog/everparse-hard... https://lwn.net/Articles/770750/ https://lwn.net/Articles/770750/ https://project-everest.github.io/ https://project-everest.github.io/
- nextaccountic 2mo agoFirefox cryptographic primitives are written and formally verified in F* Some Windows things too I think (I think F* is partially funded by Microsoft Research) They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementations https://project-everest.github.io/ https://project-everest.github.io/ https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ https://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)
- LelouBil 2mo agohttps://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
- _doctor_love 2mo agoLooks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?
- _thejanus_ 2mo agoYes, I’ve used the EverParse lib, as well as low* extensively! I found a really nice use case, low* makes writing bare metal protocol parsers incredibly easy and compositional at no obvious cost to performance. It’s a real breath of fresh air compared to writing one giant horrible whole loop, but it basically optimises down to the same assembly.
- vivzkestrel 2mo ago- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust
- bmitc 2mo agoThat language is basically F#, except for perhaps the performance claims. But F# is definitely not a slow language.
- grndn 2mo agoMatthew Crews has a done a number of videos on high-performance F# and there are some things you can do that give a big boost over the default coding approach. Why F# for Performance -- https://www.youtube.com/watch?v=EIBRoNEpg6c https://www.youtube.com/watch?v=EIBRoNEpg6c F# for Performance-Critical Code -- https://www.youtube.com/watch?v=NZ5Lwzrdoe8 https://www.youtube.com/watch?v=NZ5Lwzrdoe8
- fluoridation 2mo agoYour question is why don't we have a language that performs much better than the best-performing languages? Why would you expect such a thing?
- vivzkestrel 2mo ago- another stupid question: what exactly makes the best performing languages perform so - c gets compiled to obj files and these are run natively by each cpu are they not? - isnt there a way to say translate a high level language directly into higly optimized machine code very specific to each processor model in the world? arent there like only a 100 processor models at max?
- aw1621107 2mo ago> what exactly makes the best performing languages perform so There's a multitude of factors. Broadly speaking, to achieve high performance on modern hardware you want one or more of: - Control over emitted code and/or data structures. You tend to see this most prominently with "low-level" programming languages like C or C++, especially when coupled with extensions like SIMD intrinsics or inline assembly. - Semantics/features that make life easier for the optimizer/runtime. Types are an obvious example here, but other things like annotations (e.g., `restrict` in C, `std::unreachable` or `[[likely]]`/`[[unlikely]]` in C++) and the right abstractions (e.g., C++ expression templates) can all make it easier to get good performance. - Less dynamic semantics. Stuff that changes or needs to be resolved at runtime tends to make optimizers/hardware unhappy, so if you want performance you either want to avoid writing such constructs in the first place (e.g., writing code that doesn't involve pointer chasing) or spend engineering effort to reduce/eliminate their impact at runtime (e.g., the JVM, though for best effect you tend to need to write your code in a specific style anyways). There's probably other factors I'm forgetting... > c gets compiled to obj files and these are run natively by each cpu are they not? To a first approximation, sure. > isnt there a way to say translate a high level language directly into higly optimized machine code very specific to each processor model in the world? This is basically one of the things JITs promise - the ability to optimize a program specifically for the computer it is running on. It's technically possible to offer processor-specific binaries with ahead-of-time compilation as well (e.g., passing the appropriate -march flag to GCC/Clang/etc.), but I think for most programs you'll usually see different binaries for different CPU families based on the instruction set(s) they implement (e.g., one binary for x86-64v2, one for x86-64v3, one for x86-64v4, etc.) rather than processor-specific binaries.