Gonna nerd-snipe you with F* 😉

fstar-lang.org/

"is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving."

E.g. proving function equivalence:
floss.social/@janriemer/114446…

Crazy language! 😄

@lambdageek

I'm not sure.

github.com/ucsd-progsys/liquid…

it looks like maybe it will work.

although I don't know if there's any meaningful interaction between the linear and refinement types

LiquidHaskell binary does not work with LinearTypes · Issue #1887 · ucsd-progsys/liquidhaskell

Running the binary for liquidhaskell-0.8.10.2 on any file containing a pragma for the LinearTypes language extension returns this: » liquid .hs liquid: Unsupported extension: LinearTypes Is t...

^GitHub

@DesChips I'd be curious yes. However if you were about to explain the type/subtype distinction to me, I have received that help already in the time since my post: mastodon.social/@mcc/114535020…

Thanks

mcc

2025-05-19 14:41:50

@eggrobin Hi, sorry… are you saying that

`type Nonzero is new Natural range 1..Natural'Last;`

is introducing the hard "no mixing!" nominal type, whereas

`subtype Nonzero is new Natural range 1..Natural'Last;`

is just like creating a shorthand expansion for `Natural range 1..whatever`, and would have evaded my error above?

Sub-types are indeed important ^^ What I noticed first is that you use anonymous subtypes and constraints a lot, where I would define explicit types. For example, with the array of integers:

type Mem_Length is range 0 .. 20_000;

type Any_Mem_Element is new Integer range -1 .. Integer'Last;
Invalid : constant Any_Mem_Element := -1;
subtype Valid_Mem_Element is Any_Mem_Element range 0 .. Any_Mem_Element'Last;

type Mem_Array is array (Mem_Length range <>) of Any_Mem_Element;

Then you can declare your array like so:

Mem_Len : constant Mem_Length := 42;
Memory : Mem_array (1 .. Mem_Len) := (others => Invalid);

You can also check for valid elements, e.g.:
for Elt of Memory loop
if Elt in Valid_Mem_Element then
--- something
end if;
end loop;

@DesChips This is fascinating! I'm confused by the '(others => Invalid)' value being assigned to Memory in the line

Memory : Mem_array (1 .. Mem_Len) := (others => Invalid);

Mem_Len (set to 42) is limited to the range 0 .. 20000. In the assignment of (others => Invalid), what are the 42 elements of Memory assigned to -- Invalid? Or something else (or undefined, which seems very anti-Ada)? Or is Invalid returned if Memory is accessed with an index outside 1 .. 42, i.e. 0, 43 .. 20000?

I guess I'm mostly confused by what 'others' refers to.

@arclight When "others" is alone in the array literal (aggregate) it means all the elements of the array. Which, in this case, I set to the value of the "Invalid" constant. The word "others" makes more sense when you provide values from some elements of the array and a default value for all other elements, e.g.:

Memory : Mem_array (1 .. Mem_Len) := (1 => 2, 4 => 0, 16 => 13, others => Invalid);

learn.adacore.com/courses/intr…

“learn.adacore.com"

An interactive learning platform to teach the Ada and SPARK programming languages.

^{learn.adacore.com}

@arclight

It's just a constant declared to be the value -1 (matching what you have in the code screenshots in this thread). It's an actual byte value that you can store in a variable of type Any_Mem_Element.

A : Any_Mem_Element := Invalid.

and then I excluded this value from the Valid_Mem_Element subtype by defining the range from 0 to last:

subtype Valid_Mem_Element is Any_Mem_Element range 0 .. Any_Mem_Element'Last;