Suzette Haden Elgin created the Laadan language with a grammar that includes the source of knowledge in how assertions are stated. This reminds me of how Agda allows the inclusion of proofs about the data within its data structures.