The seven specification ur-languages • Hacker News Board

Re: The seven specification ur-languages

#51

Post by cratermoon » Tue, May 09, 2023, 8:10 PM UTC

culi wrote: post #31

simiansays wrote: post #2

> All taxonomies are broken, full stop. Your categories are gonna be completely wrong and everybody’s going to argue over every single thing. There is no such thing as a tree. Is this a serious statement? If so, wouldn't it be incompatible with the theory of evolution? Would an alien taxonomy of human binary numbers not be a legitimate tree?

> If so, wouldn't it be incompatible with the theory of evolution? It's very much not. The thing is that every model is a lie, but they can often be very useful lies. The reason we use taxonomic trees is because they're "good enough" but there are tons of places where this really breaks down. For example, horizontal gene transfer is a huge problem in microorganisms. If you take a soil fungi from one environment and p…

One word: siphonophores

Re: The seven specification ur-languages

#52

Post by mcguire » Tue, May 09, 2023, 8:19 PM UTC

Heh, eh, well, ah, ... (and other strange noises).

Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.)

Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY (A Discipline of Multiprogramming, Springer-Verlag, 2001.) or Mohamed Gouda's Abstract Protocols (Elements of network protocol design, Whiley 2008.)

Re: The seven specification ur-languages

#53

Post by madhadron » Tue, May 09, 2023, 8:19 PM UTC

simiansays wrote: post #2

> All taxonomies are broken, full stop. Your categories are gonna be completely wrong and everybody’s going to argue over every single thing. There is no such thing as a tree. Is this a serious statement? If so, wouldn't it be incompatible with the theory of evolution? Would an alien taxonomy of human binary numbers not be a legitimate tree?

I spent some time working on replacing the formulation of descent as a tree of species with a chain-complete partial order of organisms. Then you start trying to define things like "species" or "strain" or "genus" on that and realize that they don't correspond to any typical clumping of graphs.

Someone else already linked to ring species. In microbiology, the definition of species is "stop asking, we agreed to stop fighting about that, no, really, la-la-la-la." Horizontal gene transfer between species is ubiquitous.

In the end I started talking about populations occupying a niche in a specific place at a specific time, and very cautiously tracing properties among linkages of those. But I'm also the one who kept insisting to my labmates that a gene is not a locus of DNA.

Re: The seven specification ur-languages

#54

Post by mcguire » Tue, May 09, 2023, 8:20 PM UTC

simiansays wrote: post #2

> All taxonomies are broken, full stop. Your categories are gonna be completely wrong and everybody’s going to argue over every single thing. There is no such thing as a tree. Is this a serious statement? If so, wouldn't it be incompatible with the theory of evolution? Would an alien taxonomy of human binary numbers not be a legitimate tree?

Have you ever heard a discussion betweeen biologists about where to put a given species in the family tree?

Taxonomies are a human construction.

Re: The seven specification ur-languages

#55

Post by hwayne » Tue, May 09, 2023, 8:21 PM UTC

mcguire wrote: post #52

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY ( A Discipline of Multiprogrammi…

there are too many specification languages

Re: The seven specification ur-languages

#56

Post by User23 » Tue, May 09, 2023, 8:28 PM UTC

mcguire wrote: post #52

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY ( A Discipline of Multiprogrammi…

> Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.)

This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined by Dijkstra and Scholten (among others, but they're the ones best known to me). So in that sense the ur-language for program specification is something we might call "mathematical logic." And predicate transformer semantics, when you get right down to it, is leaning on Leibniz's principle about as hard as biology leans on H-bonds. As you say, GCL is just a simple language that has a well defined predicate transformer semantic and an interesting approach to nondeterminism that is suitable for the kind of research Dijkstra was doing. One could theoretically define predicate transformer semantics for any language, although it would be a prohibitively difficult challenge for most if not all languages in common use today. Whether that's a problem with predicate transformer semantics or the languages we have is a matter of opinion I suppose.

Also predicate transformer semantics were extended to support concurrency by Lamport[1].

I'm still hoping for the day when assertional arguments fully banish behavioral ones, but it looks like it's still a long way off.

[1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf

Re: The seven specification ur-languages

#57

Post by mcguire » Tue, May 09, 2023, 8:31 PM UTC

hwayne wrote: post #55

mcguire wrote: post #52

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY ( A Discipline of Multiprogrammi…

there are too many specification languages

Ooohhhh, a specification language for specification languages.

The grammar that ties together graphical things like Petri Nets and TLA+ is going to be fantastic!

Re: The seven specification ur-languages

#58

Post by culi » Tue, May 09, 2023, 8:36 PM UTC

cratermoon wrote: post #51

culi wrote: post #31

Earlier quoted context omitted.

> If so, wouldn't it be incompatible with the theory of evolution? It's very much not. The thing is that every model is a lie, but they can often be very useful lies. The reason we use taxonomic trees is because they're "good enough" but there are tons of places where this really breaks down. For example, horizontal gene transfer is a huge problem in microorganisms. If you take a soil fungi from one environment and p…

One word: siphonophores

(I mentioned them already :P)

Re: The seven specification ur-languages

#59

Post by mcguire » Tue, May 09, 2023, 8:42 PM UTC

User23 wrote: post #56

mcguire wrote: post #52

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY ( A Discipline of Multiprogrammi…

> Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined b…

For some reason, I ended up calling those "axiomatic semantics"; predicate transformer semantics is a much better name.

One of the weaknesses of PTS for common languages is that statements and expressions have very complicated semantics, compared to the relatively simple semantics of GCL and other simple treatments. One of the nice things about Frama-C (and I think the GNAT SPARK tools) is that, when you are using the WP (Weakest Precondition) module to prove properties of C code, it can automatically generate assertions that describe overflow/underflow, which then forces you to put the appropriate preconditions on function parameters. :-)

By the way, have you run across K. Rustan M. Leino's recent book, Program Proofs, and the Dafny language. It's the most recent and so far, best book I've seen on the style and technology.

Re: The seven specification ur-languages

#60

Post by hwayne » Tue, May 09, 2023, 8:50 PM UTC

mcguire wrote: post #57

hwayne wrote: post #55

Earlier quoted context omitted.

there are too many specification languages

Ooohhhh, a specification language for specification languages. The grammar that ties together graphical things like Petri Nets and TLA+ is going to be fantastic!

Unrelated but the coolest thing I discovered while researching this piece was that Petri Net reachability is decidable but Ackermann-complete. ACK-COMPLETE is a thing. That's wild.