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 team was not.
I never really got to use it, and all I've ever done with it is a few of the toy examples on their website, but I haven't completely given up on it either. I think it's a much more approachable system than Coq or Agda, but still gives you sexy dependent types.
My PhD stuff is in Isabelle, and I do really like Isabelle, but I find that dependent types translate a bit more directly to "real code" than Isabelle's higher-order logic, so I would really like to utilize it for something, particularly with its .NET integration.
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-world use cases where this could really be applied?
F* existed before Project Everest, but Everest did power a lot of its development.
We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/
The Everest project did publish a proved TLS implementation: https://mitls.org.
And at least the EverCrypt* cryptographic primitives has been used outside of academia.
I have not tried the VSCode stuff, but I did try the Emacs thing. Looking at the repo you linked, it looks like the first commit was last year and I left Jet in 2018.
The Emacs mode was fine, I didn't think it was bad, but it was still a tough sell to my team; none of them wanted to install Emacs, they wanted a Visual Studio or JetBrains experience. I'm aware that's an uphill battle, and maybe it would be a different story if the VSCode extension existed in 2018.
I didn't find F# so hard to run in production, particularly after JetBrains released Rider, but even before that I didn't think it was so bad.
At Jet we managed to get to pretty decent scale with F#, and for the most part got pretty ok performance. Often I would use the C# versions of libraries simply because they were updated more frequently. Everyone says that the C# interop is clunky and I think that's just not true, I found it relatively easy to work with C# libraries and utilize the .NET Framework. I used ConcurrentDictionary and SemaphoreSlim pretty heavily, for example. For the stuff was a little cludgy, I found it pretty straightforward to simply make wrapper functions that did what I needed.
I even found the object-oriented support in F# to be pleasant, though I didn't use it a lot. The syntax was really terse but easy to read, so in the rare cases where I had to extend a class or something, it wasn't hard. If I needed to implement an interface, it was also pretty easy to write an anonymous interface and plop that into a wrapper function.
One thing that I didn't like about F# was the kind of unpredictable performance with the async monad. It was hard to measure, and it didn't seem to work completely deterministically due to some kind of laziness that I never completely understood. The task monad released a bit later seemed to fix that, but that was integrated a bit later than my time at Jet.
Still, I found it a pretty decent language, to a point where if I started a company I would genuinely consider utilizing F#.
I haven't really used the Ionide plugin for VSCode, but I did make pretty liberal use of the Emacs plugin (well, Spacemacs), and it was pretty solid. I used it almost exclusively for about a year; I don't know if the Emacs plugin uses Ionide behind the scenes, but I thought it was pretty decent overall.
Still, once Rider got a few updates and was stable, it was kind of hard to go back. I'm a pretty dedicated Vim dude normally, but for a lot of "enterprisey" things like .NET and Java the ability to do smart refactoring of lots of files and integrated debuggers really do become a pretty substantial value-add for me.
I was working for Jet.com, it was one of the very few places that did F#. The reason I was hired was because I had Haskell experience from working at NYU as an engineer before.
I used F# at realtyshares in 2017. Didn't think it was particularly great for anything except Payment processing. The F# tools were only good with VS IDE on Windows at the time. I would probably use it again though, the REPL is much better than anything C# has to offer.
The Rider release was a shitshow, lots of bugs that went unfixed. Productivity went way down when I had to switch to a mac laptop (keep in mind this is 2017 on a Microsoft language). Had similar experiences with Rubymine in 2022 (poor YARD support, lots of bugs in type inference even with simple things, bug tickets left open for years, thank god for Sorbet-lsp). The tooling is probably better these days but I don't trust Jetbrains for anything, they are a rent-seeking company.
Maybe try looking for Clojure jobs? They aren't super common but are a lot more so than any other lisps or functional languages that I'm aware of (except maybe Scala).
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.
Lean is lovely, but those of us using it for general purpose programming are a lonely bunch; virtually all discussion on Zulip is about mathlib and tactics (which is understandable).
I have heard of Lean, but I just took a look for the first time. Certainly, much more Idris/Haskelly than the OCamlish F*.
Are there libraries available for general programming in Lean? Can you compile to another lower-level language like C?
I would be interested in writing some embedded code that could formally be verified. Right now, I have put some time in to SPARK2014, the subset of Ada.
Lean in fact compiles to C so the C FFI is trivial to use. However, the only general programming facilities Lean has seem to be those required to bootstrap the language. I find it equal amounts funny and sad that you still cannot get the Unix epoch in Lean; you need to call the C functions through the FFI.
For verifying code Lean is not great right now (see a sibling comment in this post). For embedded code in particular, I remember there was a low-level formalizer, but I cannot remember what it was. This post here has many discussions and links: https://news.ycombinator.com/item?id=31775216
But I was under the impression there was an almost assembly-level functional programming language with formal verification capabilities; I cannot recall it.
Thanks, I had looked at ATS many years ago, but I had forgotten about it. I'm going to look at both Lean and ATS, but I guess I'll stick with SPARK2014 for work now.
I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking changes, and so on.
Some day, I'd love to write proofs instead of tests in some places.
While I agree with that in principal, in talking to people who have actually written proved programs I get the impression they don't think it is practical to prove programs that are more than medium sized. I'd love to prove my code correct, but I deal with 10s of million lines of code and nobody has a clue how you would approach a problem that large (we use C++, but you can select a different language if you want - the problem is the size and you can't get around that with a different language
I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps it's writing the automation that is hard right now due to a small overlap in skills.
Writing the proofs is one thing but writing the automation that scales those proofs to a larger system and which makes it easy to extend the system without breaking the proofs constantly is key and requires more "engineering" focused people rather than proof-focused ones.
I've talked to people on both sides of that question. Some think you can (but have had little success in convincing anyone to do it), others think you cannot.
Divide and conquer does work a bit, though. Languages that support strong encapsulation of various structures will be easier to work with than those that pass pointers around.
As an example, having proofs of various properties of strcat, strcpy, etc. will help less in large programs than having proofs for all Java’s methods on String. In the former, you’ll also have to proof that covers all accesses to your data. In the latter, the JVM guarantees that.
Surely it wouldn't be aimed at proving a 10 million line black box of code, right?
In my mind it would have to be built from the ground up, sub unit tests for function proofs and maintain 100% coverage as you go along. As long as the constituent parts are proven you don't have to zoom out to a macro level.
This "function" has a superficial similarity to unsafePerformIO but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the IO monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet.
Yeah, it's pretty funny to see the first draft of anything I'm trying to prove; it'll be polluted with sorry's everywhere; it comes off as the most apologetic, completely un-confident bit of math you can think of.
The worst part is when you forget to remove a sorry (or three) because of a linked file you didn't check, and you submit stuff to other people on the team thinking you discovered something pretty cool, only to find out that you didn't actually prove anything.
"Obviously" casts a nice aspersion upon anyone so uncouth as to question its validity.
Of course, any junior member of a team that is willing to stand up and state that, no, the assertion is anything but obvious to them, should get an immediate promotion, and be quickly moved to another group!
Well Coq is used to build a C compiler used in aerospace. At the very least you could write "trricky" stuff in that, and then use the compiled artefacts in your toolkit.
I get the general complaint, though. I wish I could have the syntax-based interactive proof system everywhere.
I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either because we're iterating, or because features aren't used anymore. Also, bugs aren't the end of the world most of the time. You don't aim for 100% correctness, but for something that provides value to users and it's better than your competitors. Formal proofs may be useful in some case, but I don't see them outside very niche fields. Even regular static types can be argued against.
It seems a practical system would do all of the above:
- attempt a proof, could pass or fail, but if it times out, then fall back to...
- property-based test case generation, using logical statements and data generators, shrinking, etc.; many will pass, some will fail, but if some time out ...
- generate simple tests, and edge cases, which may trivially pass, but could be edited by hand to become more useful
If you add a timeout, then exponential runtimes, and even the Halting Problem, always give an answer, even if the answer is to try something simpler.
For small projects without tight performance or reliability requirements, Lean 4 is fine. It is lacking a lot in basic I/O functions, but you just yank them directly from the C standard library via the FFI and use them in your code. Don't expect to be able to prove anything about your code, though; just treat Lean as a pure functional language like Haskell but with dependent types and eager default evaluation.
In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?
By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them.
[Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect LISP style ergonomics here. It doesn't help that the meta-programming book shows some trivial examples of macro rules and then delves deep into proof tactics for the next 2 chapters, leaving the reader who wants general code transformations stranded].
In order to use Lean for proving properties for serious amounts of code, you need to write an entire tactics library similar to mathlib (but for code). Nobody has done this. Maybe it is reasonably hard, or maybe unreasonably hard; the point is, there is no serious collaborative effort that I know of.
Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me.
The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.
Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.
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. Plus the legacy is immense for Ada and SPARK2014.
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?
SPARK's pre-/postconditions and assertions can be statically checked, they aren't just for runtime enforcement. This is its key value proposition, if it were just runtime enforcement it'd be nice, but not that great.
I thought the partnership was already over? AdaCore left Ferrocene, and released its own support for a Rust toolchain lacking formal verification tools.
Very well might be the case. I am speaking on old news. I would guess the lack of an official published standard makes it hard to create tools and support them over time - a moving target.
As someone only dimly aware of this space, I wish upfront they would highlight what they see as their relative strengths to similar systems and techniques. For example, I'm aware that both NuPRL and Coq have some ability to extract programs from proofs. What kinds of problems does F* do better at? Are there some areas where the SMT solver is a particular advantage? Are the extracted programs superior in some way?
F* has an extraction backend which targets "human-readable C" code, contrarily to Coq which extracts proof to "machine-written OCaml" (typically the extracted code use a type-system-escape-hatch left in OCaml for the sake of Coq extraction). Consequently, part of the Everest project (the proven cryptographic primitives in particular) has been integrated into C code base like the linux kernel, firefox .
I think humanity in general are only dimly aware of this space. The Research section is probably your best bet about what's different. I think your questions are what academics call "open".
They wrapped Dijkstra and Scholten's predicate transformer semantics [2] in a monad[1]! This almost irrationally pleases me. I'd really love the general concept to get wider traction too. While it's particularly useful for this kind of deep language design, a weakest precondition calculus be used manually when writing code[3] without any particular additional effort once proficiency has been achieved. To use an analogy, it's like the old trick of solving a maze by starting at the end and working backward. Often it ends up being considerably easier.
[3] It pretty much boils down to looking at your code and asking yourself "what has to be true for this to work?" and then writing code that ensures whatever is necessary is true for all possible code paths. Naturally that means limiting possible code paths. There's just one more reason why spaghetti code is bad.
They internalize it with tacit assumptions and let runtime exceptions deal with it when the assumptions are violated. We all do this to some extent, and not just in programming, but many people are a lot more YOLO about it when the language allows it (see “duck typing”)
It takes effort for me to compute whether grandfather is de gauche or de droite.. the better question to ask yourself continuously is whether: does this noise
(spaghetti/imprecision in this context)
improve or remove performance
((0-1) though the 2 questions are related; it's enough to point out that if necessity is the mother of invention, then paradox is the father of discovery)?
Everyone, even the atheist furry and the cis-Baptist, professes belief in equal outcomes for equal situations; the problems arise both because we all have differing discretion functions to determine situations given facts and law, and because we all have different equivalence* relations on outcomes.
All a n i m a l s are e q u a l
(but some are more equal than others)
* consider reflexive vs irreflexive symmetric transitive rel'ns, or the US doctrine of "separate but equal" (1896-1954)
Not me :) unequal outcomes is either plain observation, or fantasy --- only, the latter only, I might deign to call "beliefs".. Given, some may put observation and fantasy in the same equivalence class, I should like to encounter them. (Talented SWEs?/intermediate reppers(aka designers)?)
just skimming a poorly translated and poorly formatted english version of K,AN as viewed by his students...
> Perhaps Andrey Nikolaevich's approach to teaching was also influenced by the free postgraduate existence, which he later recalled
as his happiest time. At that time, a graduate student was supposed to pass 14 exams in 14 different mathematical sciences. But the exam could be replaced by an independent result in the relevant field. Andrey Nikolaevich
said that he never passed a single exam, but instead wrote
14 articles on various topics with new results. "One of the results,
concluded Andrey Nikolaevich, "turned out to be incorrect, but I realized this after the exam was completed."
Now, that is the good stuff: Нужны Парижу деньги се ля ви / А рыцари ему нужны тем паче!
while I'm thinking about it: Kuznets waves remind me of buffering behaviour in chemistry — or bufferbloat across routers. (end of random synaptic activation)
thanks for these and the other (sps)! atm I'm busy altering the position of matter at or near the earth's surface relative to other matter, so it may be a week or two before I'm back to the more intellectual exercise of altering the truthiness of symbols in strings or graphs relative to other symbols...
Ah what shall we do if our beloved HN weren't an obligate asynchrotroph :) Passive consumption recommendation (fit for travel plausibly even) is: to «Das Glasperlenspiel» the postpostmodern (but merely pre-eschatological) riposte could only be «Anathem» --- had to complete the commutative diagram.
Ah, but the kernel between Hesse and Stephenson is fairly large; I'd say Hesse has a large idea (Berlin's "hedgehog") towards which his characters and plots and settings all work, while Stephenson has a cornucopia of small ideas (Berlin's "fox") and his characters and plots and settings are largely excuses to get them all out of his head and down in print.
My diagram would be: (Exercise: who is the contemporary hedgehog X?)
Hesse ---------> Pynchon
| |
| |
V V
X ----------> Stephenson
[to what degree are foxes cohedgehogs, or hedgehogs cofoxes? can we get the plurality of ideas of a fox by reversing arrows such that each of the fox's multiple ideas maps back, in the image, to a shared thematic point?]
Will have to woolgather/think about this, but I wonder if it might not be easier (for now, for me) to frame your question(s) in terms of a short exact sequence, with Hesse squarely in the middle, of course.
I agree that Pynchon was more or less an aloof observer of the von Neumann denouement.. maybe you can have Lem in your corner depending on how optimistic you think he is, but I would put Kim Stanley Robinson in that corner (been thinking about the Mondragon Accord). The median HN'er, I don't know, Iain Banks/Gibson. Feel free to take it to another level with some cryptic pointers (/arrows) :)
H
https://en.wikipedia.org/wiki/Mondragon_Corporation#Mondrago...
And checkout KSR's influences.
I admit to not having read <<DGPS>> in its entirety (or any majority,really) -- reason being that I read Demian E2E and surmised that the apple hedgehog didn't land too far from the tree fox. Trying to reconsider now :)
Just going by publication date alone, I think Das Glasperlenspiel (1943) will be concretely different from Demian (1919). Like Zweig's Schachnovelle (1942), the question of how should/could intellectuals share a world with power-seeking anti-intellectuals* was, in the early 1940s, far from an abstraction.
(if you have a personality suitable to attempt inner emigration, you can claim the State, as an object with little intellectual content, is maya, mere illusion, but like Berkeley's [well, Johnson's] rock it usually sullenly refuses to wither away even if you don't believe in it. cf PKD)
* on that theme: "They delight in acting in bad faith, since they seek not to persuade by sound argument but to intimidate and disconcert." is another change rung.
Re: Mondragon, compare https://www.igalia.com (how many of these are there?); the CNT may have lost at the barricades (and half-star forts), but there are still sparks among their embers?
The (mafic?) object of 18 May brings us right back to JvN and prediction vs control. Depending upon how isotropic a skipping stone one picks, the resulting trajectory may be predictable or chaotic: in a world of too cheap-to-meter compute and effectors, one might imagine a "skipping stone" with LEDs and some kind of mechanical effectors that could be used to write Peristence-of-Vision messages by "skipping" it across a lake surface?
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 Karamel, funny.
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.
I'm guessing they came up with the wordplay before the invasion, and then regretted it because the reference suddenly stopped being purely historical.
And I get it, I've been phasing out this username, which I picked with bad timing, to avoid unintended connotations, even though I was simply thinking of Robotnik and not anything russian. I've got nothing to do with their language, so it just isn't worth it.
I, personally, am aware, but I'm not so sure everyone who will read my username knows that, and there's enough war-related shilling around (and suspicion thereof) that the pun simply isn't worth it.
Well tbf Kremlin (as typically used) isn’t just a USSR reference it’s a specific place in Moscow. Still used as a metonym for Russia’s government.
That said I do actually love that Soviet propaganda aesthetic. Can appreciate not wanting to be associated with the existing madman running Russia though.
"Coon - new tool for building Erlang packages, dependency management and deploying Erlang services" [0] comes to mind. Highly recommendable thread to read.
It's odd how this is deemed acceptable - Wikipedia explains that the joke is in reference to its "brutal" optimization, which I'm sure eastern Europeans find hilarious (they might, they're known for their grim sense of humour) - but no one would seriously consider naming, say, their fork of the GNU assembler "Hitler".
Stalin never earned the same perception as Hitler, probably because he won and Hitler didn't. History is written by the victors. There's a reason the cliche move in politics is to call your opponent "literally Hitler" and not "literally Stalin". That said, I doubt any tool named "Stalin" would gain any major traction. Adopting such a tool would be a huge liability for a company.
I always figured this would be the correct name for a tool designed to erase unwanted objects out of photos (whether using classic techniques or AI, whatever).
Correct me if I'm wrong (I've only dabbled in F* and only briefly read about 1ML) but wouldn't F*'s full dependent types make 1ML redundant?
That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexities they bring.
Interesting point. I never inferred a strong connection between dependent types and the unification of records and modules. Maybe a real PL theorist around here can provide insights on that subject.
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 relationship to or level of interoperability with F#, if there is any?
I never really got to use it, and all I've ever done with it is a few of the toy examples on their website, but I haven't completely given up on it either. I think it's a much more approachable system than Coq or Agda, but still gives you sexy dependent types.
My PhD stuff is in Isabelle, and I do really like Isabelle, but I find that dependent types translate a bit more directly to "real code" than Isabelle's higher-order logic, so I would really like to utilize it for something, particularly with its .NET integration.