F* – A Proof-Oriented Programming Language • Hacker News Board

Re: F* – A Proof-Oriented Programming Language

#91

Post by 082349872349872 » Sat, May 18, 2024, 10:59 AM UTC

vinnyvichy wrote: post #85

082349872349872 wrote: post #83

Earlier quoted context omitted.

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. (0) https://ironichles.livejournal.com/56695.html

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

Compare https://en.wikipedia.org/wiki/Cyril_M._Kornbluth#Personality... (and some of YT's more discursive HN commentary).

[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?]

Re: F* – A Proof-Oriented Programming Language

#92

Post by 082349872349872 » Sat, May 18, 2024, 11:11 AM UTC

vinnyvichy wrote: post #80

082349872349872 wrote: post #49

Earlier quoted context omitted.

> looking at your code and asking yourself "what has to be true for this to work?" Wait a moment: are there people who write and ship code without continually asking this question, at least to handwaving precision?

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)? (0-1) https://quillette.com/2022/04…

Just an aside on Henderson:

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)

Re: F* – A Proof-Oriented Programming Language

#93

Post by ykonstant » Sat, May 18, 2024, 12:28 PM UTC

Tainnor wrote: post #88

ykonstant wrote: post #70

Earlier quoted context omitted.

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 Ha…

I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?

I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really:

- I like Lean's inductive type system much better that Haskell's,

- I prefer eager evaluation by default,

- I like the syntax better,

- I like dependent types; they are dangerous, but it is great to have the option.

I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with either, so I don't know about that.

Re: F* – A Proof-Oriented Programming Language

#94

Post by Tainnor » Sun, May 19, 2024, 6:34 AM UTC

ykonstant wrote: post #93

Tainnor wrote: post #88

Earlier quoted context omitted.

I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?

I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really: - I like Lean's inductive type system much better that Haskell's, - I prefer eager evaluation by default, - I like the syntax better, - I like dependent types; they are dangerous, but it is great to have the option. I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with ei…

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.

Re: F* – A Proof-Oriented Programming Language

#95

Post by vinnyvichy » Mon, May 20, 2024, 1:37 AM UTC

082349872349872 wrote: post #91

vinnyvichy wrote: post #85

Earlier quoted context omitted.

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. (0) https://ironichles.livejournal.com/56695.html

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 hedge…

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 > 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 :)

Re: F* – A Proof-Oriented Programming Language

#96

Post by vinnyvichy » Mon, May 20, 2024, 2:10 AM UTC

082349872349872 wrote: post #92

vinnyvichy wrote: post #80

Earlier quoted context omitted.

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)? (0-1) https://quillette.com/2022/04…

Just an aside on Henderson: 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…

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)?)

EDIT: in case you missed it, follow-up on ANK (not KANs) https://scottaaronson.blog/?p=762

Re: F* – A Proof-Oriented Programming Language

#97

Post by vinnyvichy » Mon, May 20, 2024, 9:08 AM UTC

vinnyvichy wrote: post #95

082349872349872 wrote: post #91

Earlier quoted context omitted.

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 hedge…

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 th…

Also, Platonov.

https://socialecologies.wordpress.com/2015/07/05/reading-and...

Re: F* – A Proof-Oriented Programming Language

#98

Post by 082349872349872 » Mon, May 20, 2024, 10:19 AM UTC

vinnyvichy wrote: post #95

082349872349872 wrote: post #91

Earlier quoted context omitted.

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 hedge…

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 th…

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?

Re: F* – A Proof-Oriented Programming Language

#99

Post by vinnyvichy » Tue, May 21, 2024, 4:12 AM UTC

082349872349872 wrote: post #98

vinnyvichy wrote: post #95

Earlier quoted context omitted.

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 th…

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?

I hear Portugal (not, specifically, the Man) is trying to host a Cambrian.

Sorry, you have to find citations for that, should be an interesting exercise

Re: F* – A Proof-Oriented Programming Language

#100

Post by 082349872349872 » Wed, May 22, 2024, 1:04 AM UTC

vinnyvichy wrote: post #95

082349872349872 wrote: post #91

Earlier quoted context omitted.

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 hedge…

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 th…

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.