Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

fstar-lang.org

Post reply on HN
Print view View original

71–80 of 107 posts

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

#71

Post by sqlserver2008 »

giancarlostoro wrote: post #33
sroerick wrote: post #16

Earlier quoted context omitted.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

Sure but even with no code indentation at all, an auto-formatter can easily indent everything for you because of the braces. If you have poorly indented code in a language like Python, you're on the hook for indenting everything yourself. And as a bonus, the code won't even run until you do.

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

#72

Post by giancarlostoro »

koolala wrote: post #34
giancarlostoro wrote: post #33

Earlier quoted context omitted.

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

Isn't it easy to just auto format it?

You mean add indentation to code where it shouldn't matter?

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

#73

Post by dataflow »

sroerick wrote: post #16
rixed wrote: post #12

Earlier quoted context omitted.

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.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

Honestly, I wouldn't worry about this. Indentation never got in the way of Python's success. There are plenty other things to worry about besides this.

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

#74

Post by _doctor_love »

cyanregiment wrote: post #67
Verdex wrote: post #66

Earlier quoted context omitted.

Meanwhile I'm sure there's people out there baffled that anyone finds dwarf fortress challenging to get into. I'm old enough that I've had the pleasure of handholding software engineers through their first anonymous function usage. Effect system, refinement types, totality checker? The best I get is blank stares before they go back to C# and JavaScript. These days I'm just glad they tolerate linq expressions and type…

> These days I'm just glad they tolerate linq expressions and typescript If it walks like a duck, farts like a dog, and flies like a fish - it's Java$cript. TypeScript is used by the pious - they think it will bring them closer to God. > dwarf fortresses that prove code with math And then there's you guys. Gattir allar, aþr gangi fram, vm scoðaz scyli, vm scygnaz scyli; þviat ouist er at vita, hvar ovinir sitia a fle…

Breathes there the man, with soul so dead,

Who never to himself hath said,

This is my own, my native land!

Whose heart hath ne’er within him burn’d,

As home his footsteps he hath turn’d,

From wandering on a foreign strand!

If such there breathe, go, mark him well;

For him no Minstrel raptures swell;

High though his titles, proud his name,

Boundless his wealth as wish can claim;

Despite those titles, power, and pelf,

The wretch, concentred all in self,

Living, shall forfeit fair renown,

And, doubly dying, shall go down

To the vile dust, from whence he sprung,

Unwept, unhonour’d, and unsung.

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

#75

Post by AdieuToLogic »

giancarlostoro wrote: post #33
sroerick wrote: post #16

Earlier quoted context omitted.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

> I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

And I love that people love indentation based languages so I show them a file with some spurious tabs to see how they feel about indentation causing silent errors.

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

#76

Post by galangalalgol »

_doctor_love wrote: post #74
cyanregiment wrote: post #67

Earlier quoted context omitted.

> These days I'm just glad they tolerate linq expressions and typescript If it walks like a duck, farts like a dog, and flies like a fish - it's Java$cript. TypeScript is used by the pious - they think it will bring them closer to God. > dwarf fortresses that prove code with math And then there's you guys. Gattir allar, aþr gangi fram, vm scoðaz scyli, vm scygnaz scyli; þviat ouist er at vita, hvar ovinir sitia a fle…

Breathes there the man, with soul so dead, Who never to himself hath said, This is my own, my native land! Whose heart hath ne’er within him burn’d, As home his footsteps he hath turn’d, From wandering on a foreign strand! If such there breathe, go, mark him well; For him no Minstrel raptures swell; High though his titles, proud his name, Boundless his wealth as wish can claim; Despite those titles, power, and pelf,…

How does this relate to the topic? I'm willing to assume it does, I just don't get it. I'm probably overreacting because when Scott was writing this, tens of thousands of Scots living in poverty were being evicted via arson from their land and country. Saying they were dead in spirit is very elitist as he sat in comfort.

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

#77

Post by a1j9o94 »

aleph_minus_one wrote: post #65
cyanregiment wrote: post #51

Earlier quoted context omitted.

> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...]. Ok, what kinds of problems are they? And ideally - what does a simple solution look like in F-star? Set me on the path to installing the thing (ideally above the fold)

> Ok, what kinds of problems are they? > And ideally - what does a simple solution look like in F-star? RTFM Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example. > Set me on the path to installing the thing (ideally above the fold) How to install this thing: 1. Read https://fstar-lang.org/index.html#download 2.…

You are right that someone could go through that effort bat that only really makes sense if they give you some.idea how to use it.

Reading the exchange it seems like you got caught up on the illustrative examples the other person used. If a web server isn't a good example of a simple problem for F* the landing page should have an example of something that is. It shouldn't take going through that many steps to understand the so what.

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

#78

Post by nickpsecurity »

dnautics wrote: post #61
3lambda wrote: post #15

Would this language be useful for implementing compilers and formally proving things about them?

personally 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.

They 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.

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

#79

Post by floxy »

Georgelemental wrote: post #54
sroerick wrote: post #16

Earlier quoted context omitted.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

Indentation based is a pain when copy-pasting between contexts with different indentation levels, as you have to fix it up manually, which is error-prone. In languages without it, you can just auto-format. (And even in an editor that doesn't support that, having a second indicator makes it less error-prone to fix manually)

>copy-pasting

Underappreciated benefit of side benefit of indentation based languages: no copy-pasta.

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

#80

Post by koolala »

giancarlostoro wrote: post #72
koolala wrote: post #34

Earlier quoted context omitted.

Isn't it easy to just auto format it?

You mean add indentation to code where it shouldn't matter?

We need auto-unformatting too? Auto formatting that doesn't get added as a git change?
Post reply on HN