Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

9.2K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#agda

2 posts2 participants1 post today
Public
Christian Tietze

I wonder why some programing communities still use abbreviated symbol identifiers.

E.g. the #Agda Programming Language Foundations book using "Can" instead of "Canonical".

90% of the code is auto-generatable by filling type holes anyway; why stick to short names that make it even more concise to the point of being harder to follow as a reader?

Public *
Jesper Agdakx 🔸

As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

tudelft.fra1.qualtrics.comType-Driven Development in PracticeUnderstanding the usage and state of tools and languages for Type-Driven Development
#Agda#Coq#Rocq
Continued thread
Public *
Tom de Jong

It turns out there is an even simpler example of a set that "fails" (in a much stronger sense) to have at most one tight apartness, following an idea of @aws.

Suppose ℕ has at most one tight apartness.
We show that double negation elimination (¬¬P ⇒ P for all P) holds.

Since ℕ is discrete (i.e. it has decidable equality), the relation ≠ is a tight apartness.

Let P be an arbitrary proposition.
The relation n ♯ m := P ∧ (n ≠ m) on ℕ is an apartness.
Furthermore, it is tight if we assume ¬¬P.
But it clearly coincides with ≠ if and only if P holds.

Thus, if the natural numbers have at most one tight apartness then double negation elimination, or equivalently excluded middle, holds.
Moreover, this generalizes to any discrete type with two distinct points.

The above is formalized in TypeTopology using #Agda, see martinescardo.github.io/TypeTo

martinescardo.github.ioApartness.Properties
ExploreLive feeds
About